def
Lean.Meta.Grind.Arith.Linear.getStructId?.go?.checkToFieldDefEq?
(type : Expr)
(u : Level)
(parentInst? inst? : Option Expr)
(toFieldName : Name)
:
Equations
- One or more equations did not get rendered due to their size.
- Lean.Meta.Grind.Arith.Linear.getStructId?.go?.checkToFieldDefEq? type u (some inst) inst? toFieldName = pure none
- Lean.Meta.Grind.Arith.Linear.getStructId?.go?.checkToFieldDefEq? type u parentInst? inst? toFieldName = pure none