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ᵢ.

instance Aesop.instInhabitedSubstitution : Inhabited Substitution

instance Aesop.Substitution.instBEq : BEq Substitution

instance Aesop.Substitution.instHashable : Hashable Substitution

instance Aesop.Substitution.instOrd : Ord Substitution

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

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

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.

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.

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.

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.

instance Aesop.Substitution.instToMessageData : Lean.ToMessageData Substitution

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.

def Aesop.Substitution.containsHyp (hyp : Lean.FVarId) (s : Substitution) : Bool

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

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.

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.

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.