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