def Aesop.RuleTac.forwardHypPrefix : Lean.Name

Equations

• Aesop.RuleTac.forwardHypPrefix = `fwd

def Aesop.RuleTac.forwardImplDetailHypPrefix : Lean.Name

Equations

• Aesop.RuleTac.forwardImplDetailHypPrefix = `_fwd

def Aesop.RuleTac.mkFreshForwardImplDetailHypName : Lean.MetaM Lean.Name

Equations

• Aesop.RuleTac.mkFreshForwardImplDetailHypName = Lean.Meta.mkFreshIdWithPrefix Aesop.RuleTac.forwardImplDetailHypPrefix

def Aesop.RuleTac.isForwardImplDetailHypName (n : Lean.Name) : Bool

Equations

• Aesop.RuleTac.isForwardImplDetailHypName n = Lean.Name.isPrefixOf Aesop.RuleTac.forwardImplDetailHypPrefix n

def Aesop.RuleTac.getForwardHypTypes : Lean.MetaM (Lean.HashSet Lean.Expr)

Equations

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

def Aesop.RuleTac.applyForwardRule (goal : Lean.MVarId) (e : Lean.Expr) (pat? : Option Aesop.RulePattern) (patInsts : Lean.HashSet Aesop.RulePatternInstantiation) (immediate : Aesop.UnorderedArraySet Nat) (clear : Bool) (generateScript : Bool) (md : Lean.Meta.TransparencyMode) : Lean.MetaM (Lean.MVarId × Option Aesop.RuleTacScriptBuilder)

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 __do_lift ← Lean.Meta.mkConstWithFreshMVarLevels decl Aesop.RuleTac.forwardExpr __do_lift 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.