git.iko.soy/Idris-dev
on master help sign in
Idris-dev/test/regression002/Mod.idr
12 lines 142 B history raw
1module Mod
3-- %access public
5export
6natfn : Nat -> Nat
7natfn n = (S (S n))
9public export
10natexp : (n : Nat) -> Nat
11natexp k = S (natfn k)