Skip to content
Snippets Groups Projects
Commit be38c833 authored by Amin Timany's avatar Amin Timany
Browse files

Apply 1 suggestion(s) to 1 file(s)

parent f9c33304
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris_staging/algebra/monotone.v
+ 1
− 1
View file @ be38c833
...@@ -15,7 +15,7 @@ Local Arguments cmra_valid _ !_ /. ...@@ -15,7 +15,7 @@ Local Arguments cmra_valid _ !_ /.
(* Given a preorder relation R on a type A we construct a resource algebra mra R (* Given a preorder relation R on a type A we construct a resource algebra mra R
and an injection principal : A -> mra R such that: and an injection principal : A -> mra R such that:
R x y iff principal x ≼ principal y [R x y] iff [principal x ≼ principal y]
where ≼ is the extension order of mra R resource algebra. This is exactly where ≼ is the extension order of mra R resource algebra. This is exactly
what the lemma [principal_included] shows. what the lemma [principal_included] shows.
......
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