Abstract binding trees are a generic representation of terms over a given signature
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`
MkArgument : List kind -> kind -> Argument
.binders : Argument -> List kind
binders : Argument -> List kind
.argType : Argument -> kind
argType : Argument -> kind
0 Signature : Type
A signature is a relation describing constructors.
Each constructor has a list of arguments and a return type.
data Term : Signature -> SnocList kind -> kind -> Type
data Args : Signature -> SnocList kind -> List Argument -> Type
lift : (Elem s ctx -> Elem s ctx') -> Elem s (ctx :< t) -> Elem s (ctx' :< t)
lifts : (bds : List kind) -> (Elem s ctx -> Elem s ctx') -> Elem s (ctx <>< bds) -> Elem s (ctx' <>< bds)
rename : (Elem s ctx -> Elem s ctx') -> Term sig ctx s -> Term sig ctx' s
renames : (Elem s ctx -> Elem s ctx') -> Args sig ctx args -> Args sig ctx' args
extend : (Elem s ctx -> Term sig ctx' s) -> Elem s (ctx :< t) -> Term sig (ctx' :< t) s
extends : (bds : List kind) -> (Elem s ctx -> Term sig ctx' s) -> Elem s (ctx <>< bds) -> Term sig (ctx' <>< bds) s
substitute : (Elem s ctx -> Term sig ctx' s) -> Term sig ctx s -> Term sig ctx' s
substitutes : (Elem s ctx -> Term sig ctx' s) -> Args sig ctx args -> Args sig ctx' args