Documentation

Aesop.Forward.Substitution

A substitution for the premises of a rule. Given a rule with type ∀ (x₁ : T₁) ... (xₙ : Tₙ), U a substitution is a finite partial map with domain {1, ..., n} that associates an expression with some or all of the premises.

  • premises : Array (Option RPINF)

    The substitution.

  • The level substitution implied by the premise substitution. If e is the elaborated rule expression (with level params replaced by level mvars), and collectLevelMVars (← instantiateMVars e) = [?m₁, ..., ?mₙ], then levels[i] is the level assigned to ?mᵢ.

Instances For
def Aesop.Substitution.empty (numPremises numLevels : Nat) :

The empty substitution for a rule with the given number of premise indexes.

Equations

Insert the mapping pi ↦ inst into the substitution s. Precondition: pi is in the domain of s.

Equations

Get the instantiation associated with premise pi in s. Precondition: pi is in the domain of s.

Equations

Insert the mapping li ↦ inst into the substitution s. Precondition: li is in the domain of s and inst is normalised.

Equations

Get the instantiation associated with level li in s. Precondition: li is in the domain of s.

Equations
Equations
  • One or more equations did not get rendered due to their size.

Merge two substitutions. Precondition: the substitutions are compatible, so they must have the same size and if s₁[x] and s₂[x] are both defined, they must be the same value.

Equations
  • One or more equations did not get rendered due to their size.

Returns true if any expression in the codomain of s contains hyp.

Equations

Given e with type ∀ (x₁ : T₁) ... (xₙ : Tₙ), U and a substitution σ for the arguments xᵢ, replace occurrences of xᵢ in the body U with fresh metavariables (like forallMetaTelescope). Then, for each mapping xᵢ ↦ tᵢ in σ, assign tᵢ to the metavariable corresponding to xᵢ. Returns the newly created metavariables (which may be assigned!), their binder infos and the updated body.

Equations
  • One or more equations did not get rendered due to their size.

Given rule of type ∀ (x₁ : T₁) ... (xₙ : Tₙ), U and a substitution σ for the arguments xᵢ, specialise rule with the arguments given by σ. That is, construct U t₁ ... tₙ where tⱼ is σ(xⱼ) if xⱼ ∈ dom(σ) and is otherwise a fresh fvar, then λ-abstract the fresh fvars.

Equations
  • One or more equations did not get rendered due to their size.

Open the type of a rule e. If a substitution σ is given, this function acts like Substitution.openRuleType σ. Otherwise it acts like forallMetaTelescope.

Equations