def Aesop.RuleTac.makeForwardHyps (e : Lean.Expr) (pat? : Option Aesop.RulePattern) (patInst : Aesop.RulePatternInstantiation) (immediate : Aesop.UnorderedArraySet Nat) (maxDepth? : Option Nat) (forwardHypData : Aesop.ForwardHypData) : Lean.MetaM (Array (Lean.Expr × Nat) × Array Lean.FVarId)

Equations

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

partial def Aesop.RuleTac.makeForwardHyps.loop (maxDepth? : Option Nat) (forwardHypData : Aesop.ForwardHypData) (app : Lean.Expr) (instMVars : Array Lean.MVarId) (immediateMVars : Array Lean.MVarId) (i : Nat) (proofsAcc : Array (Lean.Expr × Nat)) (currentMaxHypDepth : Nat) (currentUsedHyps : Array Lean.FVarId) (usedHypsAcc : Array Lean.FVarId) (proofTypesAcc : Std.HashSet Lean.Expr) : Lean.MetaM (Array (Lean.Expr × Nat) × Array Lean.FVarId × Std.HashSet Lean.Expr)

def Aesop.RuleTac.assertForwardHyp (goal : Lean.MVarId) (hyp : Lean.Meta.Hypothesis) (depth : Nat) (md : Lean.Meta.TransparencyMode) : Aesop.ScriptM (Lean.FVarId × Lean.MVarId)

Equations

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

def Aesop.RuleTac.assertForwardHyp.tacticBuilder (goal : Lean.MVarId) (hyp : Lean.Meta.Hypothesis) (md : Lean.Meta.TransparencyMode) : Lean.FVarId × Lean.MVarId → Aesop.Script.TacticBuilder

Equations

• Aesop.RuleTac.assertForwardHyp.tacticBuilder goal hyp md x = Aesop.Script.TacticBuilder.assertHypothesis goal hyp md

def Aesop.RuleTac.applyForwardRule (goal : Lean.MVarId) (e : Lean.Expr) (pat? : Option Aesop.RulePattern) (patInsts : Std.HashSet Aesop.RulePatternInstantiation) (immediate : Aesop.UnorderedArraySet Nat) (clear : Bool) (md : Lean.Meta.TransparencyMode) (maxDepth? : Option Nat) : Aesop.ScriptM Aesop.Subgoal

Equations

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

def Aesop.RuleTac.applyForwardRule.err (e : Lean.Expr) {α : Type} : Lean.MetaM α

Equations

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

@[inline]

def Aesop.RuleTac.forwardExpr (e : Lean.Expr) (pat? : Option Aesop.RulePattern) (immediate : Aesop.UnorderedArraySet Nat) (clear : Bool) (md : Lean.Meta.TransparencyMode) : Aesop.RuleTac

Equations

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

def Aesop.RuleTac.forwardConst (decl : Lean.Name) (pat? : Option Aesop.RulePattern) (immediate : Aesop.UnorderedArraySet Nat) (clear : Bool) (md : Lean.Meta.TransparencyMode) : Aesop.RuleTac

Equations

• Aesop.RuleTac.forwardConst decl pat? immediate clear md input = do let e ← Lean.Meta.mkConstWithFreshMVarLevels decl Aesop.RuleTac.forwardExpr e pat? immediate clear md input

def Aesop.RuleTac.forwardTerm (stx : Lean.Term) (pat? : Option Aesop.RulePattern) (immediate : Aesop.UnorderedArraySet Nat) (clear : Bool) (md : Lean.Meta.TransparencyMode) : Aesop.RuleTac

Equations

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

def Aesop.RuleTac.forward (t : Aesop.RuleTerm) (pat? : Option Aesop.RulePattern) (immediate : Aesop.UnorderedArraySet Nat) (clear : Bool) (md : Lean.Meta.TransparencyMode) : Aesop.RuleTac

Equations

• Aesop.RuleTac.forward (Aesop.RuleTerm.const decl) pat? immediate clear md = Aesop.RuleTac.forwardConst decl pat? immediate clear md
• Aesop.RuleTac.forward (Aesop.RuleTerm.term tm) pat? immediate clear md = Aesop.RuleTac.forwardTerm tm pat? immediate clear md