Mercurial > hg > Papers > 2021 > soto-prosym

comparison Paper/src/cbc-agda.agda.replaced @ 2:9176dff8f38a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ADD while loop description
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Fri, 05 Nov 2021 15:19:08 +0900
parents c59202657321
children 339fb67b4375
comparison
equal deleted inserted replaced
1:3910f4639344 2:9176dff8f38a
1 plus : {l : Level} {t : Set l} @$\rightarrow$@ (x y : @$\mathbb{N}$@) @$\rightarrow$@ (next : @$\mathbb{N}$@ @$\rightarrow$@ t) @$\rightarrow$@ t 1 module cbc-agda where
2 plus x zero next = next x 2
3 plus x (suc y) next = plus (suc x) y next 3 open import Data.Nat
4 open import Level renaming ( suc to succ ; zero to Zero )
5
6 record Env : Set where
7 field
8 varx : @$\mathbb{N}$@
9 vary : @$\mathbb{N}$@
10 open Env
11
12 plus-com : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
13 plus-com env next exit with vary env
14 ... | zero = exit (record { varx = varx env ; vary = vary env })
15 ... | suc y = next (record { varx = suc (varx env) ; vary = y })
16
17 {-@$\#$@ TERMINATING @$\#$@-}
18 plus-p : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t
19 plus-p env exit = plus-com env ( @$\lambda$@ env @$\rightarrow$@ plus-p env exit ) exit
20
21 plus : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Env
22 plus x y = plus-p (record { varx = x ; vary = y }) (@$\lambda$@ env @$\rightarrow$@ env)