- data Path : Nat -> Type
- Totality: total
Constructors:
- Here : Path 0
- Left : Path n -> Path (S n)
- Right : Path n -> Path (S n)
- data Tree : Nat -> Type -> Type
- Totality: total
Constructors:
- Leaf : a -> Tree 0 a
- Node : Tree n a -> Tree n a -> Tree (S n) a
- fromNat : (k : Nat) -> (n : Nat) -> (0 _ : LT k (pow2 n)) -> Path n
Convert a natural number to a path in a perfect binary tree
Totality: total- fromNatCorrect : (k : Nat) -> (n : Nat) -> (0 p : LT k (pow2 n)) -> toNat (fromNat k n p) = k
The `fromNat` conversion is compatible with the semantics `toNat`
Totality: total- lookup : Tree n a -> Path n -> a
- Totality: total
- replicate : (n : Nat) -> a -> Tree n a
- Totality: total
- toNat : Path n -> Nat
- Totality: total
- toNatBounded : (n : Nat) -> (p : Path n) -> LT (toNat p) (pow2 n)
- Totality: total