Idris2Doc : Data.Telescope.Segment

Data.Telescope.Segment

A segment is a compositional fragment of a telescope.
A key difference is that segments are right-nested, whereas
telescopes are left nested.
So telescopes are convenient for well-bracketing dependencies,
but segments are convenient for processing telescopes from left
to right.

As with telescopes, indexing segments by their length (hopefully)
helps the type-checker infer stuff.
(++) : (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
dataEnvironment : Environmentgamma -> Segmentngamma -> Type
Totality: total
Constructors:
Empty : Environmentenv []
(.=) : (x : tyenv) -> Environment (MkDPairenvx) delta -> Environmentenv (ty::delta)
dataSegment : Nat -> Telescopek -> Type
  A segment is a compositional fragment of a telescope, indexed by
the segment's length.

Totality: total
Constructors:
Nil : Segment0gamma
(::) : (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 -> Segmentk []
  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 : Segmentk [] -> 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