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 aa58011 commit a537d5cCopy full SHA for a537d5c
1 file changed
src/Iris/Algebra/DFrac.lean
@@ -19,7 +19,7 @@ abbrev DFrac F := LeibnizO (DFracK F)
19
20
-- TODO: Delete this class. I have it now because the Fractional class is being
21
-- changed concurrently. Also I'm certain that some of these fields will be derivable.
22
-class DFractional (F : Type _) extends Fractional F where
+class DFractional (F : Type _) extends UFractional F where
23
-- one_strict_max {y : F} : ¬(One.one + y ≤ One.one)
24
-- lt_irrefl : ¬(One.one < (One.one : F))
25
-- strict_pos {x y : F} : ¬(x + y = x)
0 commit comments