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 = plusAcc m n

Totality: total
Visibility: export

plusAccZeroRightNeutral : (m : Nat) -> plusAcc m 0 = m

Totality: total
Visibility: public export

data Telescope : Nat -> Type

  A left-nested sequence of dependent types

Totality: total
Visibility: public export
Constructors:

Nil : Telescope 0

(-.) : (gamma : Telescope k) -> TypeIn gamma -> Telescope (S k)

TypeIn : Telescope k -> Type

  A type with dependencies in the given context

Totality: total
Visibility: public export

Environment : Telescope k -> Type

  A tuple of values of each type in the telescope

Totality: total
Visibility: public export

weakenTypeIn : TypeIn gamma -> TypeIn (gamma -. sigma)

Totality: total
Visibility: export

uncons : (gamma : Telescope (S k)) -> (ty : Type ** (delta : ty -> Telescope k ** (v : ty) -> Environment (delta v) -> Environment gamma))

Totality: total
Visibility: public export

(++) : (gamma : Telescope m) -> (Environment gamma -> Telescope n) -> Telescope (plusAcc n m)

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

cons : (ty : Type) -> (ty -> Telescope k) -> Telescope (S k)

Totality: total
Visibility: public export
Fixity Declarations:
infixr operator, level 5
infixr operator, level 5

Position : Telescope k -> 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 : Telescope k) -> Position gamma

  The position at the beginning of the telescope

Totality: total
Visibility: public export

data Telescope : Nat -> Type

  A right-nested sequence of dependent types

Totality: total
Visibility: public export
Constructors:

Nil : Telescope 0

(.-) : (ty : Type) -> (ty -> Telescope k) -> Telescope (S k)

Environment : Telescope k -> Type

  A tuple of values of each type in the telescope

Totality: total
Visibility: public export

empty : (0 gamma : Telescope 0) -> Environment gamma

Totality: total
Visibility: export

snoc : (gamma : Telescope k) -> (Environment gamma -> Type) -> Telescope (S k)

Totality: total
Visibility: export
Fixity Declarations:
infixl operator, level 5
infixl operator, level 5

unsnoc : (gamma : Telescope (S k)) -> (delta : Telescope k ** (sigma : Environment delta -> Type ** (env : Environment delta) -> sigma env -> Environment gamma))

Totality: total
Visibility: export

(++) : (gamma : Telescope m) -> (Environment gamma -> Telescope n) -> Telescope (m + n)

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

split : (gamma : Telescope m) -> (delta : (Environment gamma -> Telescope n)) -> Environment (gamma ++ delta) -> (env : Environment gamma ** Environment (delta env))

Totality: total
Visibility: export

data Telescope : Nat -> Type

  A tree of dependent types

Totality: total
Visibility: public export
Constructors:

Nil : Telescope 0

Elt : Type -> Telescope 1

(><) : (gamma : Telescope m) -> (Environment gamma -> Telescope n) -> Telescope (m + n)

Environment : Telescope k -> Type

  A tuple of values of each type in the telescope

Totality: total
Visibility: public export

concat : (gamma : Telescope k) -> (delta : Telescope k ** Environment delta -> Environment gamma)

Totality: total
Visibility: export

(<++>) : (gamma : Telescope m) -> (Environment gamma -> Telescope n) -> Telescope (plusAcc m n)

Totality: total
Visibility: public export
Fixity Declarations:
infix operator, level 5
infixr operator, level 5

leftToRight : Telescope m -> Telescope m

Totality: total
Visibility: export

rightToLeft : Telescope m -> Telescope m

Totality: total
Visibility: export