Idris2Doc : Data.Telescope.Telescope

Data.Telescope.Telescope

The telescope data structures.

Indexing telescopes by their length (hopefully) helps inform the
type-checker during inference.
(<++>) : (gamma : Telescope m) -> (Environment gamma -> Telescope n) -> Telescope (plusAcc m n)
Totality: total
Fixity Declaration: infix operator, level 5
leftToRight : Telescope m -> Telescope m
Totality: total
plusAcc : Nat -> Nat -> Nat
Totality: total
plusAccIsPlus : (m : Nat) -> (n : Nat) -> m + n = plusAcc m n
Totality: total
plusAccZeroRightNeutral : (m : Nat) -> plusAcc m 0 = m
Totality: total
rightToLeft : Telescope m -> Telescope m
Totality: total