--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/agda/cbc-agda.agda	Tue Feb 09 18:44:53 2021 +0900
@@ -0,0 +1,22 @@
+module cbc-agda where
+
+open import Data.Nat
+open import Level renaming ( suc to succ ; zero to Zero )
+
+record Env : Set where
+  field
+    varx : ℕ
+    vary : ℕ
+open Env
+
+plus-com : {l : Level} {t : Set l} → Env → (next : Env → t) → (exit : Env → t) → t
+plus-com env next exit with vary env
+... | zero  = exit (record { varx = varx env ; vary = vary env })
+... | suc y = next (record { varx = suc (varx env) ; vary = y })
+
+{-# TERMINATING #-}
+plus-p : {l : Level} {t : Set l} → (env : Env) → (exit : Env → t) → t
+plus-p env exit = plus-com env ( λ env → plus-p env exit ) exit
+
+plus : ℕ → ℕ → Env
+plus x y = plus-p (record { varx = x ; vary = y }) (λ env → env)