def Lean.Meta.Grind.isCastLikeDeclName (declName : Name) : Bool

Returns true if declName is the name of a cast-like function used to implement grind solvers

Equations

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

def Lean.Meta.Grind.isCastLikeFn (f : Expr) : Bool

Returns true if f is a cast-like operation.

Equations

• Lean.Meta.Grind.isCastLikeFn (Lean.Expr.const declName us) = (pure (Lean.Meta.Grind.isCastLikeDeclName declName)).run
• Lean.Meta.Grind.isCastLikeFn f = (pure false).run

def Lean.Meta.Grind.isCastLikeApp (e : Expr) : Bool

Equations

• Lean.Meta.Grind.isCastLikeApp e = Lean.Meta.Grind.isCastLikeFn e.getAppFn