annotate paper/src/AgdaPlus.agda.replaced @ 4:bf1f62556b81

add while_test_init_imple
author soto
date Thu, 11 Feb 2021 17:03:31 +0900
parents 959f4b34d6f4
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
3
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
1 _+_ : Nat @$\rightarrow$@ Nat @$\rightarrow$@ Nat
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
2 zero + m = m
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
3 suc n + m = suc (n + m)