0
|
1 data nomal-tree (A : Set) : Set where
|
5
|
2 nleaf : (key : !$\mathbb{N}$!) !$\rightarrow$! tree A
|
|
3 nnode : (key : !$\mathbb{N}$!) !$\rightarrow$! (lnode : nomal-tree A) !$\rightarrow$! (rnode : nomal-tree A) !$\rightarrow$! nomal-tree A
|
0
|
4
|
5
|
5 data meta-tree (A : Set) : (key : !$\mathbb{N}$!) !$\rightarrow$! Set where
|
|
6 mleaf : (key : !$\mathbb{N}$!) !$\rightarrow$! meta-tree A key
|
|
7 mnode : { l r : !$\mathbb{N}$! } !$\rightarrow$! (key : !$\mathbb{N}$!) !$\rightarrow$! (value : A)
|
|
8 !$\rightarrow$! (lnode : meta-tree A l) !$\rightarrow$! (rnode : meta-tree A r)
|
|
9 !$\rightarrow$! l !$\leq$! key !$\rightarrow$! key !$\leq$! r !$\rightarrow$! metatree A key
|
0
|
10
|