Skip to content
Snippets Groups Projects
Commit f2be3543 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Rename `cmra_monotone_valid` into `cmra_morphism_valid`.

parent f72ef909
No related branches found
No related tags found
No related merge requests found
......@@ -769,7 +769,7 @@ Section cmra_morphism.
Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.
Lemma cmra_morphism_monotoneN n x y : x {n} y f x {n} f y.
Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.
Lemma cmra_monotone_valid x : x f x.
Lemma cmra_morphism_valid x : x f x.
Proof. rewrite !cmra_valid_validN; eauto using cmra_morphism_validN. Qed.
End cmra_morphism.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment