Mercurial > hg > Papers > 2021 > soto-prosym
diff Paper/src/bt_impl/bt_env.agda @ 5:339fb67b4375
INIT rbt.agda
author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 07 Nov 2021 00:51:16 +0900 |
parents | |
children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/bt_impl/bt_env.agda Sun Nov 07 00:51:16 2021 +0900 @@ -0,0 +1,12 @@ +data bt {n : Level} (A : Set n) : Set n where + leaf : bt A + node : (key : ℕ) → (value : A) → + (left : bt A ) → (right : bt A ) → bt A + +record Env {n : Level} (A : Set n) : Set n where + field + varn : ℕ + varv : A + vart : bt A + varl : List (bt A) +open Env \ No newline at end of file