log
graph
tags
bookmarks
branches
changeset
browse
file
latest
diff
comparison
annotate
file log
raw
help
Mercurial
>
hg
>
Papers
>
2021
>
soto-thesis
annotate prepaper/src/NatAdd.agda @ 0:
3dba680da508
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
init-test
author
soto
date
Tue, 08 Dec 2020 19:06:49 +0900
parents
children
Ignore whitespace changes -
Everywhere:
Within whitespace:
At end of lines:
rev
line source
0
3dba680da508
init-test
soto
parents:
diff
changeset
1
open import nat
3dba680da508
init-test
soto
parents:
diff
changeset
2
module nat_add where
3dba680da508
init-test
soto
parents:
diff
changeset
3
3dba680da508
init-test
soto
parents:
diff
changeset
4
_+_ : Nat -> Nat -> Nat
3dba680da508
init-test
soto
parents:
diff
changeset
5
O + m = m
3dba680da508
init-test
soto
parents:
diff
changeset
6
(S n) + m = S (n + m)