Core.TT.Term.Subst

Definitions

SubstEnv : Scope -> Scoped

Totality: total
Visibility: public export

substs : SizeOf dropped -> SubstEnv dropped vars -> Term (dropped ++ vars) -> Term vars

Totality: total
Visibility: export

subst : Term vars -> Term (bind vars x) -> Term vars

Totality: total
Visibility: export