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

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

Returns true if f is a cast-like operation.

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