Core.TT.Subst

Definitions

data Subst : Scoped -> Scope -> Scoped

Totality: total
Visibility: public export
Constructors:

Nil : Subst tm empty vars

(::) : tm vars -> Subst tm ds vars -> Subst tm (d :: ds) vars

empty : Subst tm empty vars

Totality: total
Visibility: public export

index : Subst tm ds vars -> Var ds -> tm vars

Totality: total
Visibility: export

findDrop : (Var vars -> tm vars) -> SizeOf dropped -> Var (dropped ++ vars) -> Subst tm dropped vars -> tm vars

Totality: total
Visibility: export

find : Weaken tm => (Var vars -> tm vars) -> SizeOf outer -> SizeOf dropped -> Var (outer ++ (dropped ++ vars)) -> Subst tm dropped vars -> tm (outer ++ vars)

Totality: total
Visibility: export

0 Substitutable : Scoped -> Scoped -> Type

Totality: total
Visibility: public export