Mercurial > hg > Gears > GearsAgda

comparison work.agda~ @ 781:68904fdaab71

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
te
author Moririn < Moririn@cr.ie.u-ryukyu.ac.jp>
date Mon, 10 Jul 2023 19:59:14 +0900
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 781:68904fdaab71
1 module work where
2
3 open import Level hiding (suc ; zero ; _⊔_ )
4
5 open import Data.Nat hiding (compare)
6 open import Data.Nat.Properties as NatProp
7 open import Data.Maybe
8 -- open import Data.Maybe.Properties
9 open import Data.Empty
10 open import Data.List
11 open import Data.Product
12
13 open import Function as F hiding (const)
14
15 open import Relation.Binary
16 open import Relation.Binary.PropositionalEquality
17 open import Relation.Nullary
18 open import logic
19
20 data bt {n : Level} (A : Set n) : Set n where
21 leaf : bt A
22 node : (key : ℕ) → (value : A) → (left : bt A) → (right : bt A) → bt A