Idris2Doc : Data.Tree.Perfect

Data.Tree.Perfect

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