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 Lean.Expr)

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

def Aesop.instInhabitedSubstitution.default : Substitution

Equations

• Aesop.instInhabitedSubstitution.default = { premises := default, levels := default }

@[implicit_reducible]

instance Aesop.instInhabitedSubstitution : Inhabited Substitution

Equations

• Aesop.instInhabitedSubstitution = { default := Aesop.instInhabitedSubstitution.default }

@[implicit_reducible]

instance Aesop.Substitution.instBEq : BEq Substitution

Equations

• Aesop.Substitution.instBEq = { beq := fun (s₁ s₂ : Aesop.Substitution) => s₁.premises == s₂.premises }

@[implicit_reducible]

instance Aesop.Substitution.instHashable : Hashable Substitution

Equations

• Aesop.Substitution.instHashable = { hash := fun (s : Aesop.Substitution) => hash s.premises }

@[implicit_reducible]

instance Aesop.Substitution.instOrd : Ord Substitution

Equations

• Aesop.Substitution.instOrd = { compare := fun (s₁ s₂ : Aesop.Substitution) => Aesop.Substitution.instOrd._private_1 s₁ s₂ }

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

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

Equations

• Aesop.Substitution.empty numPremises numLevels = { premises := Array.replicate numPremises none, levels := Array.replicate numLevels none }

def Aesop.Substitution.insert (pi : PremiseIndex) (inst : Lean.Expr) (s : Substitution) : Substitution

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

Equations

• Aesop.Substitution.insert pi inst s = { premises := s.premises.set! pi.toNat (some inst), levels := s.levels }

def Aesop.Substitution.find? (pi : PremiseIndex) (s : Substitution) : Option Lean.Expr

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

Equations

• Aesop.Substitution.find? pi s = s.premises[pi.toNat]!

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

• Aesop.Substitution.insertLevel li inst s = { premises := s.premises, levels := s.levels.set! li.toNat (some inst) }

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

• Aesop.Substitution.findLevel? li s = s.levels[li.toNat]!

@[implicit_reducible]

instance Aesop.Substitution.instToMessageData : Lean.ToMessageData Substitution

Equations

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

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

Equations

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

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

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

Equations

• Aesop.Substitution.containsHyp hyp s = s.premises.any fun (x : Option Lean.Expr) => match x with | none => false | some e => e.containsFVar 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.

Equations

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

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.

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

• One or more equations did not get rendered due to their size.
• Aesop.openRuleType (some subst) e = Aesop.Substitution.openRuleType e subst