Language.IntrinsicTyping.ABT

Abstract binding trees are a generic representation of terms over
a given signature

Definitions

record Argument : Type

  A constructor's argument describes the kind of the variables that
  will be bound in the subterm as well as the overall type of the
  argument.
    The argument `n` in `S n`   is described by `MkArgument [] Nat`
    The argument `b` in `\x. b` is described by `MkArgument [s] t`

Totality: total
Visibility: public export
Constructor: 

MkArgument : List kind -> kind -> Argument

Projections:

.argType : Argument -> kind

.binders : Argument -> List kind

.binders : Argument -> List kind

Totality: total
Visibility: public export

binders : Argument -> List kind

Totality: total
Visibility: public export

.argType : Argument -> kind

Totality: total
Visibility: public export

argType : Argument -> kind

Totality: total
Visibility: public export

0 Signature : Type

  A signature is a relation describing constructors.
  Each constructor has a list of arguments and a return type.

Totality: total
Visibility: public export

data Term : Signature -> SnocList kind -> kind -> Type

Totality: total
Visibility: public export
Constructors:

Var : Elem s ctx -> Term sig ctx s

  Variables are represented using typed De Bruijn indices.

Con : sig args s -> Args sig ctx args -> Term sig ctx s

  Constructors are provided by the signature

data Args : Signature -> SnocList kind -> List Argument -> Type

Totality: total
Visibility: public export
Constructors:

Nil : Args sig ctx []

  Empty list

(::) : Term sig (ctx <>< bds) s -> Args sig ctx args -> Args sig ctx (MkArgument bds s :: args)

  An argument with binders `bds` and return type `s` is provided by a term
  whose scope has been extended by `bds` and whose return type is `s`.

lift : (Elem s ctx -> Elem s ctx') -> Elem s (ctx :< t) -> Elem s (ctx' :< t)

Totality: total
Visibility: public export

lifts : (bds : List kind) -> (Elem s ctx -> Elem s ctx') -> Elem s (ctx <>< bds) -> Elem s (ctx' <>< bds)

Totality: total
Visibility: public export

rename : (Elem s ctx -> Elem s ctx') -> Term sig ctx s -> Term sig ctx' s

Totality: total
Visibility: public export

renames : (Elem s ctx -> Elem s ctx') -> Args sig ctx args -> Args sig ctx' args

Totality: total
Visibility: public export

extend : (Elem s ctx -> Term sig ctx' s) -> Elem s (ctx :< t) -> Term sig (ctx' :< t) s

Totality: total
Visibility: public export

extends : (bds : List kind) -> (Elem s ctx -> Term sig ctx' s) -> Elem s (ctx <>< bds) -> Term sig (ctx' <>< bds) s

Totality: total
Visibility: public export

substitute : (Elem s ctx -> Term sig ctx' s) -> Term sig ctx s -> Term sig ctx' s

Totality: total
Visibility: public export

substitutes : (Elem s ctx -> Term sig ctx' s) -> Args sig ctx args -> Args sig ctx' args

Totality: total
Visibility: public export