We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 5fc1226 commit e9e777fCopy full SHA for e9e777f
src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean
@@ -94,7 +94,9 @@ private def processDiv (e inst a b : Expr) : RingM Unit := do
94
pushNewFact <| mkExpectedPropHint
95
(mkApp7 (mkConst ``Grind.CommRing.div_int_eqC [ring.u]) ring.type (mkNatLit c) fieldInst charInst a (mkIntLit k) reflBoolTrue)
96
expected
97
- return ()
+ else
98
+ -- TODO
99
+ return ()
100
101
/--
102
Returns `true` if `e` is a term `a/b` or `a⁻¹`.
0 commit comments