Documentation

Aesop.Forward.Substitution

source
structure Aesop.Substitution :
Type

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.

  • levels : Array (Option Lean.Level)

    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
source
instance Aesop.instInhabitedSubstitution :
Inhabited Substitution
Equations
source
instance Aesop.Substitution.instBEq :
BEq Substitution
Equations
source
instance Aesop.Substitution.instHashable :
Hashable Substitution
Equations
source
instance Aesop.Substitution.instOrd :
Ord Substitution
Equations
source
def Aesop.Substitution.empty (numPremises numLevels : Nat) :
Substitution

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

Equations
source
def Aesop.Substitution.insert (pi : PremiseIndex) (inst : RPINF) (s : Substitution) :
Substitution

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

Equations
source
def Aesop.Substitution.find? (pi : PremiseIndex) (s : Substitution) :
Option RPINF

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

Equations
source
def Aesop.Substitution.insertLevel (li : LevelIndex) (inst : Lean.Level) (s : Substitution) :
Substitution

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

Equations
source
def Aesop.Substitution.findLevel? (li : PremiseIndex) (s : Substitution) :
Option Lean.Level

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

Equations
source
instance Aesop.Substitution.instToMessageData :
Lean.ToMessageData Substitution
Equations
  • One or more equations did not get rendered due to their size.
source
def Aesop.Substitution.mergeCompatible (s₁ s₂ : Substitution) :
Substitution

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.
source
def Aesop.Substitution.containsHyp (hyp : Lean.FVarId) (s : Substitution) :
Bool

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

Equations
source
def Aesop.Substitution.openRuleType (e : Lean.Expr) (subst : Substitution) :
Lean.MetaM (Array Lean.MVarId × Array Lean.BinderInfo × Lean.Expr)

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.
source
def Aesop.Substitution.specializeRule (rule : Lean.Expr) (subst : Substitution) :
Lean.MetaM Lean.Expr

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.
source
def Aesop.openRuleType (subst? : Option Substitution) (e : Lean.Expr) :
Lean.MetaM (Array Lean.MVarId × Array Lean.BinderInfo × Lean.Expr)

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

Equations