Mercurial > hg > Papers > 2023 > soto-master

comparison Paper/src/agda/lambda.agda.replaced @ 3:c28e8156a37b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add paper init~agda
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Fri, 20 Jan 2023 13:40:03 +0900
parents a72446879486
children
comparison
equal deleted inserted replaced
2:0425278b683b 3:c28e8156a37b
17 +n a x = x a 17 +n a x = x a
18 18
19 test*2 : (a : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$! 19 test*2 : (a : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
20 test*2 a = +n a (!$\lambda$! z !$\rightarrow$! z + 2) 20 test*2 a = +n a (!$\lambda$! z !$\rightarrow$! z + 2)
21 21
22 test*2' : (a : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$! 22 test*2!$\prime$! : (a : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
23 test*2' a = +n a (!$\lambda$! z !$\rightarrow$! +n z (!$\lambda$! z !$\rightarrow$! z)) 23 test*2!$\prime$! a = +n a (!$\lambda$! z !$\rightarrow$! +n z (!$\lambda$! z !$\rightarrow$! z))
24 24
25 25
26 !$\lambda$!'+2 : (x : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$! 26 !$\lambda$!!$\prime$!+2 : (x : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
27 !$\lambda$!'+2 d = {!!} -- (!$\lambda$! x !$\rightarrow$! x +1) 27 !$\lambda$!!$\prime$!+2 d = {!!} -- (!$\lambda$! x !$\rightarrow$! x +1)
28 28