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

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.

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

Equations

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

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)