def Aesop.elabForwardRuleTerm (goal : Lean.MVarId) : RuleTerm → Lean.MetaM Lean.Expr

Elaborate the term of a forward rule in the current goal.

Equations

• Aesop.elabForwardRuleTerm goal (Aesop.RuleTerm.const n) = Lean.Meta.mkConstWithFreshMVarLevels n
• Aesop.elabForwardRuleTerm goal (Aesop.RuleTerm.term stx) = (Aesop.withFullElaboration (liftM (Aesop.elabRuleTermForApplyLikeMetaM goal stx))).run'

def Aesop.Match.initial (subst : Substitution) (isPatSubst : Bool) (forwardDeps conclusionDeps : Array PremiseIndex) : Match

Create a one-element match. subst is the substitution that results from matching a hypothesis against slot 0, or from a pattern substitution. isPatSubst is true if the substitution resulted from a rule pattern. forwardDeps are the forward dependencies of slot 0. conclusionDeps are the conclusion dependencies of the rule to which this match belongs.

Equations

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

def Aesop.Match.addHypOrPatSubst (subst : Substitution) (isPatSubst : Bool) (forwardDeps : Array PremiseIndex) (m : Match) : Match

Add a hyp or pattern substitution to the match. subst is the substitution that results from matching a hypothesis against slot m.level + 1, or from the pattern. isPatSubst is true if the substitution resulted from a pattern substitution. forwardDeps are the forward dependencies of slot m.level + 1.

Equations

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

def Aesop.Match.containsHyp (hyp : Lean.FVarId) (m : Match) : Bool

Returns true if the match contains the given hyp.

Equations

• Aesop.Match.containsHyp hyp m = m.subst.premises.any fun (x : Option Aesop.RPINF) => Option.any (fun (x : Aesop.RPINF) => x.toExpr.containsFVar hyp) x

def Aesop.Match.containsPatSubst (subst : Substitution) (m : Match) : Bool

Returns true if the match contains the given pattern substitution.

Equations

• Aesop.Match.containsPatSubst subst m = m.patInstSubsts.any fun (x : Aesop.Substitution) => x == subst

def Aesop.CompleteMatch.reconstructArgs (r : ForwardRule) (m : CompleteMatch) : Array (Option RPINF) × Array (Option Lean.Level)

Given a complete match m for r, get arguments to r contained in the match's slots and substitution. For non-immediate arguments, we return none. The returned levels are suitable assignments for the level mvars of r.

Equations

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

def Aesop.CompleteMatch.toMessageData (r : ForwardRule) (m : CompleteMatch) : Lean.MessageData

Equations

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

instance Aesop.ForwardRuleMatch.instToMessageData : Lean.ToMessageData ForwardRuleMatch

Equations

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

def Aesop.ForwardRuleMatch.foldHypsM {M : Type u_1 → Type u_2} {σ : Type u_1} [Monad M] (f : σ → Lean.FVarId → M σ) (init : σ) (m : ForwardRuleMatch) : M σ

Fold over the hypotheses contained in a match.

Equations

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

def Aesop.ForwardRuleMatch.foldHyps {σ : Type u_1} (f : σ → Lean.FVarId → σ) (init : σ) (m : ForwardRuleMatch) : σ

Fold over the hypotheses contained in a match.

Equations

• Aesop.ForwardRuleMatch.foldHyps f init m = Aesop.ForwardRuleMatch.foldHypsM f init m

def Aesop.ForwardRuleMatch.anyHyp (m : ForwardRuleMatch) (f : Lean.FVarId → Bool) : Bool

Returns true if any hypothesis contained in m satisfies f.

Equations

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

def Aesop.ForwardRuleMatch.getPropHyps (m : ForwardRuleMatch) : Lean.MetaM (Array Lean.FVarId)

Get the hypotheses from the match whose types are propositions.

Equations

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

def Aesop.ForwardRuleMatch.getProof (goal : Lean.MVarId) (m : ForwardRuleMatch) : Lean.MetaM (Option Lean.Expr)

Construct the proof of the new hypothesis represented by m.

Equations

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

def Aesop.ForwardRuleMatch.apply (goal : Lean.MVarId) (m : ForwardRuleMatch) (skip? : Option (RPINF → Bool)) : ScriptT BaseM (Option (Lean.MVarId × Lean.FVarId × Array Lean.FVarId))

Apply a forward rule match to a goal. This adds the hypothesis corresponding to the match to the local context. Returns the new goal, the added hypothesis and the hypotheses that were removed (if any). Hypotheses may be removed if the match is for a destruct rule. If the skip function, when applied to the normalised type of the new hypothesis, returns true, then the hypothesis is not added to the local context.

Equations

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

def Aesop.forwardRuleMatchesToNormRules? (ms : Array ForwardRuleMatch) : Option (Array NormRule)

Convert forward rule matches to norm rules. Fails if any of the matches is not a norm rule match.

Equations

• Aesop.forwardRuleMatchesToNormRules? ms = Aesop.forwardRuleMatchesToRules?✝ ms fun (x : Aesop.ForwardRuleMatch) => Option.map (fun (x : Int) => { penalty := x }) x.rule.prio.penalty?

def Aesop.forwardRuleMatchesToSafeRules? (ms : Array ForwardRuleMatch) : Option (Array SafeRule)

Convert forward rule matches to safe rules. Fails if any of the matches is not a safe rule match.

Equations

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

def Aesop.forwardRuleMatchesToUnsafeRules? (ms : Array ForwardRuleMatch) : Option (Array UnsafeRule)

Convert forward rule matches to unsafe rules. Fails if any of the matches is not an unsafe rule match.

Equations

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