rachel/hm
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Compare commits

base: rachel:bc7565a1f70a42e446e5f1341ba8f13dec8f129c
Branches Tags
rachel:master
..
compare: rachel:b44ffb282a07d4246bd2a48786f915472be7a3e3
Branches Tags
rachel:master

No commits in common. "bc7565a1f70a42e446e5f1341ba8f13dec8f129c" and "b44ffb282a07d4246bd2a48786f915472be7a3e3" have entirely different histories.
bc7565a1f7 ... b44ffb282a

1 changed files with 1 additions and 0 deletions
Show Stats Expand all files Collapse all files

1
test.hm
View File

@ -6,6 +6,7 @@ type Nat
-- which will bring a recursor for the type into scope -- which will bring a recursor for the type into scope
-- rec[Nat] : A → (A → A) → Nat → A -- rec[Nat] : A → (A → A) → Nat → A
-- defining addition as -- defining addition as
add : Nat → Nat → Nat add : Nat → Nat → Nat
:= rec[Nat] (λx. x) (λf n. succ (f n)) := rec[Nat] (λx. x) (λf n. succ (f n))