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.

Definitions

dataSegment : Nat->Telescopek->Type
  A segment is a compositional fragment of a telescope, indexed by
the segment's length.

Totality: total
Visibility: public export
Constructors:
Nil : Segment0gamma
(::) : (ty : TypeIngamma) ->Segmentn (gamma-.ty) ->Segment (Sn) gamma
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
Visibility: public export
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
Visibility: public export
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
Visibility: public export
toTelescope : Segmentk [] ->Telescopek
  Any segment in the empty telescope correspond to a telescope.

Totality: total
Visibility: public export
keep : (0_ : a=b) ->a=b
Totality: total
Visibility: public export
(|++) : (gamma : Telescopek) ->Segmentngamma->Telescope (n+k)
  Segments act on telescope from the right.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 3
(++) : (lft : Segmentngamma) ->Segmentm (gamma|++lft) ->Segment (n+m) gamma
  Segments form a kind of an indexed monoid w.r.t. the action `(|++)`

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7
actSegmentAssociative : (gamma : Telescopek) -> (lft : Segmentngamma) -> (rgt : Segmentm (gamma|++lft)) ->gamma|++ (lft++rgt) = (gamma|++lft) |++rgt
Totality: total
Visibility: export
weaken : TypeIngamma->TypeIn (gamma|++delta)
Totality: total
Visibility: public export
projection : Environment (gamma|++delta) ->Environmentgamma
Totality: total
Visibility: public export
dataEnvironment : Environmentgamma->Segmentngamma->Type
Totality: total
Visibility: public export
Constructors:
Empty : Environmentenv []
(.=) : (x : tyenv) ->Environment (env**x) delta->Environmentenv (ty::delta)
(:++) : (env : Environmentgamma) ->Environmentenvdelta->Environment (gamma|++delta)
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 3