Idris2Doc : Data.Telescope.Telescope

Data.Telescope.Telescope

(<++>) : (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) -> plusAccmZ = m
Totality: total
rightToLeft : Telescopem -> Telescopem
Totality: total