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

Equations

• Aesop.RuleBuilder.hasConst c e = Lean.Expr.foldConsts e 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.unfold : Aesop.RuleBuilder

Equations

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