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

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

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.

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.

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

Returns true if the match contains the given hyp.

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

Returns true if the match contains the given pattern substitution.

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.

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

instance Aesop.ForwardRuleMatch.instToMessageData : Lean.ToMessageData ForwardRuleMatch

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.

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

Fold over the hypotheses contained in a match.

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

Returns true if any hypothesis contained in m satisfies f.

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

Get the hypotheses from the match whose types are propositions.

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

Construct the proof of the new hypothesis represented by m.

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.

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.

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.

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.