[Agda] [agda2] how to programming the basic

Andreas Abel abela at chalmers.se
Sun Jan 24 09:45:13 CET 2016


"What is wrong in this picture?"

> _+2_ : Nat2 -> Nat2 -> Nat2
> zero2 *2 m = zero2
> suc n +2 m = suc (n +2 m)


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/


More information about the Agda mailing list