Idris2Doc : Data.Tree.Perfect

Data.Tree.Perfect(source)

Definitions
data Tree : Nat -> Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Leaf : a -> Tree 0 a
  
Node : Tree n a -> Tree n a -> Tree (S n) a

  Hints:
  
Applicative (Tree n)
  
Functor (Tree n)
replicate : (n : Nat) -> a -> Tree n a
  Totality: total
  Visibility: public export
data Path : Nat -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Here : Path 0
  
Left : Path n -> Path (S n)
  
Right : Path n -> Path (S n)
toNat : Path n -> Nat
  Totality: total
  Visibility: public export
toNatBounded : (n : Nat) -> (p : Path n) -> LT (toNat p) (pow2 n)
  Totality: total
  Visibility: export
data View : Nat -> Nat -> Type
  This pattern-matching in `fromNat` is annoying:
  The    `Z (S _)` case is impossible
  In the `k (S n)` case we want to branch on whether `k `LT` pow2 n`
  and get our hands on some proofs.
  This view factors out that work.

  Totality: total
  Visibility: public export
  Constructors:
  
ZZ : View 0 0
  
SLT : (0 _ : LT k (pow2 n)) -> View k (S n)
  
SNLT : (0 _ : GTE k (pow2 n)) -> (0 _ : LT (minus k (pow2 n)) (pow2 n)) -> View k (S n)
view : (k : Nat) -> (n : Nat) -> (0 _ : LT k (pow2 n)) -> View k n
  Totality: total
  Visibility: public export
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
  Visibility: public export
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
  Visibility: export
lookup : Tree n a -> Path n -> a
  Totality: total
  Visibility: public export