source
def Aesop.RuleBuilder.hasConst (c : Lean.Name) (e : Lean.Expr) :
Bool
Equations

- Aesop.RuleBuilder.hasConst c e = e.foldConsts false fun (c' : Lean.Name) (acc : Bool) => acc || c' == c

Instances For

source
def Aesop.RuleBuilder.checkUnfoldableConst (decl : Lean.Name) :
Lean.MetaM (Option Lean.Name)
Equations

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

Instances For

source
def Aesop.RuleBuilder.unfoldCore (decl : Lean.Name) :
Lean.MetaM LocalRuleSetMember
Equations

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

Instances For

source
def Aesop.RuleBuilder.unfold :
RuleBuilder
Equations

- Aesop.RuleBuilder.unfold input = do let decl ← liftM (Aesop.elabGlobalRuleIdent Aesop.BuilderName.unfold input.term) liftM (Aesop.RuleBuilder.unfoldCore decl)

Instances For