Mercurial > hg > Papers > 2021 > soto-thesis

comparison paper/src/agda/cbc-agda.agda @ 3:959f4b34d6f4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add final thesis
author soto
date Tue, 09 Feb 2021 18:44:53 +0900
parents
children
comparison
equal deleted inserted replaced
2:2c50fd1d115e 3:959f4b34d6f4
1 module cbc-agda where
2
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 : ℕ
9 vary : ℕ
10 open Env
11
12 plus-com : {l : Level} {t : Set l} → Env → (next : Env → t) → (exit : Env → t) → 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} → (env : Env) → (exit : Env → t) → t
19 plus-p env exit = plus-com env ( λ env → plus-p env exit ) exit
20
21 plus : ℕ → ℕ → Env
22 plus x y = plus-p (record { varx = x ; vary = y }) (λ env → env)