Papers/2022/soto-sigos: Paper/src/agda/lambda.agda.replaced comparison

ADD fast commit

comparison

equal deleted inserted replaced

--1:000000000000
+:14a0e409d574
+module lambda where
+open import Data.Nat
+ll+_ : (x y : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
+ll+ zero = !$\lambda$! y !$\rightarrow$! y
+ll+ suc x = !$\lambda$! y !$\rightarrow$! (ll+ x) (suc y)
+test =  (ll+ 5) 7
+-- +1をしたのち、もう一度+1をする関数を定義する場合
++1 : (x : !$\mathbb{N}$! )!$\rightarrow$! !$\mathbb{N}$!
++1 x = suc x
++n : (a : !$\mathbb{N}$!) !$\rightarrow$! (x : !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
++n a x = x a
+test*2 : (a : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
+test*2 a = +n a (!$\lambda$! z !$\rightarrow$! z + 2)
+test*2!$\prime$! : (a : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
+test*2!$\prime$! a = +n a (!$\lambda$! z !$\rightarrow$! +n z (!$\lambda$! z !$\rightarrow$! z))
+!$\lambda$!!$\prime$!+2 : (x : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$!
+!$\lambda$!!$\prime$!+2 d = {!!} -- (!$\lambda$! x !$\rightarrow$! x +1)

Mercurial > hg > Papers > 2022 > soto-sigos