Skip to content
Snippets Groups Projects
Commit 05ebd4df authored by Ralf Jung's avatar Ralf Jung
Browse files

avoid naming a typeclass argument

parent 657b34ad
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
iris/algebra/cmra.v
+ 1
− 1
View file @ 05ebd4df
...@@ -1727,7 +1727,7 @@ Section discrete_fun_cmra. ...@@ -1727,7 +1727,7 @@ Section discrete_fun_cmra.
by intros [h Hh]; exists (h x); rewrite /op /discrete_fun_op_instance (Hh x). by intros [h Hh]; exists (h x); rewrite /op /discrete_fun_op_instance (Hh x).
Qed. Qed.
Lemma discrete_fun_included_spec `{Hfin : Finite A} (f g : discrete_fun B) : Lemma discrete_fun_included_spec `{Finite A} (f g : discrete_fun B) :
f ≼ g ↔ ∀ x, f x ≼ g x. f ≼ g ↔ ∀ x, f x ≼ g x.
Proof. Proof.
split; [by intros; apply discrete_fun_included_spec_1|]. split; [by intros; apply discrete_fun_included_spec_1|].
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment