Idris2Doc : Language.IntrinsicTyping.ABT

Language.IntrinsicTyping.ABT(source)

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

Definitions

recordArgument : 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 : Listkind->kind->Argument

Projections:
.argType : Argument->kind
.binders : Argument->Listkind
.binders : Argument->Listkind
Totality: total
Visibility: public export
binders : Argument->Listkind
Totality: total
Visibility: public export
.argType : Argument->kind
Totality: total
Visibility: public export
argType : Argument->kind
Totality: total
Visibility: public export
0Signature : Type
  A signature is a relation describing constructors.
Each constructor has a list of arguments and a return type.

Totality: total
Visibility: public export
dataTerm : Signature->SnocListkind->kind->Type
Totality: total
Visibility: public export
Constructors:
Var : Elemsctx->Termsigctxs
  Variables are represented using typed De Bruijn indices.
Con : sigargss->Argssigctxargs->Termsigctxs
  Constructors are provided by the signature
dataArgs : Signature->SnocListkind->ListArgument->Type
Totality: total
Visibility: public export
Constructors:
Nil : Argssigctx []
  Empty list
(::) : Termsig (ctx<><bds) s->Argssigctxargs->Argssigctx (MkArgumentbdss::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 : (Elemsctx->Elemsctx') ->Elems (ctx:<t) ->Elems (ctx':<t)
Totality: total
Visibility: public export
lifts : (bds : Listkind) -> (Elemsctx->Elemsctx') ->Elems (ctx<><bds) ->Elems (ctx'<><bds)
Totality: total
Visibility: public export
rename : (Elemsctx->Elemsctx') ->Termsigctxs->Termsigctx's
Totality: total
Visibility: public export
renames : (Elemsctx->Elemsctx') ->Argssigctxargs->Argssigctx'args
Totality: total
Visibility: public export
extend : (Elemsctx->Termsigctx's) ->Elems (ctx:<t) ->Termsig (ctx':<t) s
Totality: total
Visibility: public export
extends : (bds : Listkind) -> (Elemsctx->Termsigctx's) ->Elems (ctx<><bds) ->Termsig (ctx'<><bds) s
Totality: total
Visibility: public export
substitute : (Elemsctx->Termsigctx's) ->Termsigctxs->Termsigctx's
Totality: total
Visibility: public export
substitutes : (Elemsctx->Termsigctx's) ->Argssigctxargs->Argssigctx'args
Totality: total
Visibility: public export