Idris2Doc : Data.Tree.Perfect

Data.Tree.Perfect

dataPath : Nat -> Type
Totality: total
Constructors:
Here : Path0
Left : Pathn -> Path (Sn)
Right : Pathn -> Path (Sn)
dataTree : Nat -> Type -> Type
Totality: total
Constructors:
Leaf : a -> Tree0a
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