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

Global Lemma → Lemma

parent 7e77c9e7
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris_staging/algebra/max_prefix_list.v
+ 2
− 2
View file @ a529364e
...@@ -39,12 +39,12 @@ Section max_prefix_list. ...@@ -39,12 +39,12 @@ Section max_prefix_list.
Global Instance mono_list_lb_core_id (m : max_prefix_list A) : CoreId m := _. Global Instance mono_list_lb_core_id (m : max_prefix_list A) : CoreId m := _.
Global Lemma to_max_prefix_list_valid l : ✓ to_max_prefix_list l. Lemma to_max_prefix_list_valid l : ✓ to_max_prefix_list l.
Proof. Proof.
intros i. rewrite /to_max_prefix_list lookup_fmap. intros i. rewrite /to_max_prefix_list lookup_fmap.
by destruct (map_seq 0 l !! i). by destruct (map_seq 0 l !! i).
Qed. Qed.
Global Lemma to_max_prefix_list_validN n l : ✓{n} to_max_prefix_list l. Lemma to_max_prefix_list_validN n l : ✓{n} to_max_prefix_list l.
Proof. apply cmra_valid_validN, to_max_prefix_list_valid. Qed. Proof. apply cmra_valid_validN, to_max_prefix_list_valid. Qed.
Local Lemma to_max_prefix_list_app l1 l2 : Local Lemma to_max_prefix_list_app l1 l2 :
......
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