Idris2Doc : Data.Telescope.Telescope

Data.Telescope.Telescope

The telescope data structures.

Indexing telescopes by their length (hopefully) helps inform the
type-checker during inference.

Definitions

plusAcc : Nat->Nat->Nat
Totality: total
Visibility: public export
plusAccIsPlus : (m : Nat) -> (n : Nat) ->m+n=plusAccmn
Totality: total
Visibility: export
plusAccZeroRightNeutral : (m : Nat) ->plusAccm0=m
Totality: total
Visibility: public export
dataTelescope : Nat->Type
  A left-nested sequence of dependent types

Totality: total
Visibility: public export
Constructors:
Nil : Telescope0
(-.) : (gamma : Telescopek) ->TypeIngamma->Telescope (Sk)
TypeIn : Telescopek->Type
  A type with dependencies in the given context

Totality: total
Visibility: public export
Environment : Telescopek->Type
  A tuple of values of each type in the telescope

Totality: total
Visibility: public export
weakenTypeIn : TypeIngamma->TypeIn (gamma-.sigma)
Totality: total
Visibility: export
uncons : (gamma : Telescope (Sk)) -> (ty : Type** (delta : ty->Telescopek** (v : ty) ->Environment (deltav) ->Environmentgamma))
Totality: total
Visibility: public export
(++) : (gamma : Telescopem) -> (Environmentgamma->Telescopen) ->Telescope (plusAccnm)
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7
cons : (ty : Type) -> (ty->Telescopek) ->Telescope (Sk)
Totality: total
Visibility: public export
Fixity Declarations:
infixr operator, level 5
infixr operator, level 5
Position : Telescopek->Type
  A position between the variables of a telescope, counting from the _end_:
Telescope: Nil -. ty1 -. ... -. tyn
Positions: ^k ^k-1 ^k-2 ^1 ^0

Totality: total
Visibility: public export
start : (gamma : Telescopek) ->Positiongamma
  The position at the beginning of the telescope

Totality: total
Visibility: public export
dataTelescope : Nat->Type
  A right-nested sequence of dependent types

Totality: total
Visibility: public export
Constructors:
Nil : Telescope0
(.-) : (ty : Type) -> (ty->Telescopek) ->Telescope (Sk)
Environment : Telescopek->Type
  A tuple of values of each type in the telescope

Totality: total
Visibility: public export
empty : (0gamma : Telescope0) ->Environmentgamma
Totality: total
Visibility: export
snoc : (gamma : Telescopek) -> (Environmentgamma->Type) ->Telescope (Sk)
Totality: total
Visibility: export
Fixity Declarations:
infixl operator, level 5
infixl operator, level 5
unsnoc : (gamma : Telescope (Sk)) -> (delta : Telescopek** (sigma : Environmentdelta->Type** (env : Environmentdelta) ->sigmaenv->Environmentgamma))
Totality: total
Visibility: export
(++) : (gamma : Telescopem) -> (Environmentgamma->Telescopen) ->Telescope (m+n)
Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7
split : (gamma : Telescopem) -> (delta : (Environmentgamma->Telescopen)) ->Environment (gamma++delta) -> (env : Environmentgamma**Environment (deltaenv))
Totality: total
Visibility: export
dataTelescope : Nat->Type
  A tree of dependent types

Totality: total
Visibility: public export
Constructors:
Nil : Telescope0
Elt : Type->Telescope1
(><) : (gamma : Telescopem) -> (Environmentgamma->Telescopen) ->Telescope (m+n)
Environment : Telescopek->Type
  A tuple of values of each type in the telescope

Totality: total
Visibility: public export
concat : (gamma : Telescopek) -> (delta : Telescopek**Environmentdelta->Environmentgamma)
Totality: total
Visibility: export
(<++>) : (gamma : Telescopem) -> (Environmentgamma->Telescopen) ->Telescope (plusAccmn)
Totality: total
Visibility: public export
Fixity Declarations:
infix operator, level 5
infixr operator, level 5
leftToRight : Telescopem->Telescopem
Totality: total
Visibility: export
rightToLeft : Telescopem->Telescopem
Totality: total
Visibility: export