|
781
|
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
|
