Agda.TypeChecking.Substitute.Class

Apply something to a bunch of arguments. Preserves blocking tags (application can never resolve blocking).

Apply to some default arguments.

Apply to a single default argument.

Apply to two default arguments.

(abstract args v) apply args --> v[args].

Apply a substitution.

Simple constraint alias for a Subst instance a with arg type t.

Subst instance whose agument type is itself

Subst instance whose argument type is Term

Raise de Bruijn index, i.e. weakening

Replace de Bruijn index i by a Term in something.

Replace what is now de Bruijn index 0, but go under n binders. substUnder n u == subst n (raise n u).

Checks whether the variable bound by the abstraction is actually used, and, if not, returns the term within, strengthened to live in the context outside the abstraction. See also isBinderUsed.

To replace index n by term u, do applySubst (singletonS n u). Γ, Δ ⊢ u : A --------------------------------- Γ, Δ ⊢ singletonS |Δ| u : Γ, A, Δ

Single substitution without disturbing any deBruijn indices. Γ, A, Δ ⊢ u : A --------------------------------- Γ, A, Δ ⊢ inplace |Δ| u : Γ, A, Δ

Lift a substitution under k binders.

       Γ ⊢ reverse vs : Δ
     -----------------------------
       Γ ⊢ parallelS vs ρ : Γ, Δ
  

Note the Γ in Γ, Δ.

Γ ⊢ (strengthenS ⊥ |Δ|) : Γ,Δ

A "smart" variant of Strengthen. If strengthenS is applied to a substitution with an outermost Strengthen constructor, then the "error message" of that constructor is discarded in favour of the Impossible argument of this function.

lookupS (listS [(x0,t0)..(xn,tn)]) xi = ti, assuming x0 < .. < xn.

Instantiate an abstraction. Strict in the term.

Instantiate an abstraction. Lazy in the term, which allow it to be IMPOSSIBLE in the case where the variable shouldn't be used but we cannot use noabsApp. Used in Apply.

Instantiate an abstraction that doesn't use its argument.