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 : Telescopem) -> (Environmentgamma -> Telescopen) -> Telescope (plusAccmn)
Totality: total
Fixity Declaration: infix operator, level 5
leftToRight : Telescopem -> Telescopem
Totality: total
plusAcc : Nat -> Nat -> Nat
Totality: total
plusAccIsPlus : (m : Nat) -> (n : Nat) -> m+n = plusAccmn
Totality: total
plusAccZeroRightNeutral : (m : Nat) -> plusAccm0 = m
Totality: total
rightToLeft : Telescopem -> Telescopem
Totality: total