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

precedence levels

Browse Source
This commit is contained in:
Rachel Lambda Samuelsson 2023-01-25 21:38:45 +01:00
parent 7fcd27aafd
commit 4d940fb59b
1 changed files with 0 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
test.hm
View File

@ -6,7 +6,6 @@ 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))