source
def Lean.Meta.Grind.Arith.CommRing.checkInst (declName : Name) (inst inst' : Expr) :
MetaM Unit
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.mkUnaryFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] (type : Expr) (u : Level) (instDeclName declName : Name) (expectedInst : Expr) :
m Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.mkBinHomoFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] (type : Expr) (u : Level) (instDeclName declName : Name) (expectedInst : Expr) :
m Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.mkPowFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] (u : Level) (type semiringInst : Expr) :
m Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.mkNatCastFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] (u : Level) (type semiringInst : Expr) :
m Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.getAddFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] :
m Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.getSubFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] :
m Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.getMulFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] :
m Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.getNegFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] :
m Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.getPowFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] :
m Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.getIntCastFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] :
m Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.getNatCastFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] :
m Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.getOne {m : Type → Type} [Monad m] [MonadCanon m] [MonadRing m] [MonadLiftT GoalM m] :
m Expr
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.CommRing.getInvFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadCommRing m] :
m Expr
Equations

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

Instances For