Idris2Doc : Data.Telescope.Segment

Data.Telescope.Segment

(++) : (lft : Segmentngamma) -> Segmentm (gamma|++lft) -> Segment (n+m) gamma
Segments form a kind of an indexed monoid w.r.t. the action `(|++)`
Totality: total
Fixity Declaration: infixl operator, level 4
(:++) : (env : Environmentgamma) -> Environmentenvdelta -> Environment (gamma|++delta)
Totality: total
Fixity Declaration: infixl operator, level 3
Environment : Environmentgamma -> Segmentngamma -> Type
Totality: total
Constructors:
Empty : EnvironmentenvNil
(.=) : (x : tyenv) -> Environment (MkDPairenvx) delta -> Environmentenv (ty::delta)
Segment : Nat -> Telescopek -> Type
A segment is a compositional fragment of a telescope, indexed by
the segment's length.
Totality: total
Constructors:
Nil : SegmentZgamma
(::) : (ty : TypeIngamma) -> Segmentn (gamma-.ty) -> Segment (Sn) gamma
actSegmentAssociative : (gamma : Telescopek) -> (lft : Segmentngamma) -> (rgt : Segmentm (gamma|++lft)) -> gamma|++ (lft++rgt) = (gamma|++lft) |++rgt
Totality: total
fromTelescope : Telescopek -> SegmentkNil
Any telescope is a segment in the empty telescope. It amounts to looking
at it left-to-right instead of right-to-left.
Totality: total
keep : (0 _ : a = b) -> a = b
Totality: total
projection : Environment (gamma|++delta) -> Environmentgamma
Totality: total
tabulate : (n : Nat) -> (Environmentgamma -> Telescopen) -> Segmentngamma
A segment of size `n` indexed by `gamma` can be seen as the tabulation of a
function that turns environments for `gamma` into telescopes of size `n`.
Totality: total
toTelescope : SegmentkNil -> Telescopek
Any segment in the empty telescope correspond to a telescope.
Totality: total
untabulate : Segmentngamma -> Environmentgamma -> Telescopen
Conversely, a segment of size `n` in telescope `gamma` can be seen as a function
from environments for `gamma` to telescopes of size `n`.
Totality: total
weaken : TypeIngamma -> TypeIn (gamma|++delta)
Totality: total
(|++) : (gamma : Telescopek) -> Segmentngamma -> Telescope (n+k)
Segments act on telescope from the right.
Totality: total
Fixity Declaration: infixl operator, level 3