Skip to content
Snippets Groups Projects
Commit ffa7e114 authored by Hai Dang's avatar Hai Dang
Browse files

fix Z scope in arc_cmra

parent 22bbf305
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/lang/arc_cmra.v
+ 1
− 0
View file @ ffa7e114
......@@ -93,6 +93,7 @@ Definition Z_of_arcstrong_st (st : strong_stUR) : Z :=
| Some (_, n) => Zpos n
end.
Local Open Scope Z_scope.
Lemma strong_stUR_value st: 0 ≤ Z_of_arcstrong_st st.
Proof. destruct st as [[]|]; simpl; lia. Qed.
......
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