We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent f50080b commit 8234092Copy full SHA for 8234092
src/Iris/Algebra/DFrac.lean
@@ -161,12 +161,6 @@ instance : CMRA.Discrete (DFrac F) where
161
162
theorem is_discrete {q : DFrac F} : OFE.DiscreteE q := ⟨congrArg id⟩
163
164
-instance : CMRA.Discrete (DFrac F) where
165
- discrete_valid {x} := by simp [CMRA.Valid, CMRA.ValidN]
166
-
167
168
169
170
theorem DFrac.update_discard {dq : DFrac F} : dq ~~> .discard := by
171
intros n q H
172
apply (CMRA.valid_iff_validN' n).mp
0 commit comments