class Lean.Meta.Sym.Arith.MonadCanon (m : Type → Type) : Type

• canonExpr : Expr → m Expr

  Canonicalize an expression (types, instances, support arguments). In SymM, this is Sym.canon. In PP.M (diagnostics), this is the identity.

• synthInstance? : Expr → m (Option Expr)

  Synthesize an instance, returning none on failure. In SymM, this is Sym.synthInstance?. In PP.M, this is Meta.synthInstance?.

@[instance_reducible, always_inline]

instance Lean.Meta.Sym.Arith.instMonadCanonOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadCanon m] : MonadCanon n

Equations

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

def Lean.Meta.Sym.Arith.MonadCanon.synthInstance {m : Type → Type} [Monad m] [MonadError m] [MonadCanon m] (type : Expr) : m Expr

Equations

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