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

fix le_upd notation

parent a32f36a9
No related branches found
No related tags found
No related merge requests found
...@@ -145,7 +145,7 @@ Module le_upd. ...@@ -145,7 +145,7 @@ Module le_upd.
Definition le_upd := le_upd_aux.(unseal). Definition le_upd := le_upd_aux.(unseal).
Local Definition le_upd_unseal : @le_upd = @le_upd_def := le_upd_aux.(seal_eq). Local Definition le_upd_unseal : @le_upd = @le_upd_def := le_upd_aux.(seal_eq).
Global Arguments le_upd {_ _} _. Global Arguments le_upd {_ _} _.
Notation "'|==£>' P" := (le_upd P) (at level 99, P at level 200, format "|==£> P"). Notation "'|==£>' P" := (le_upd P%I) (at level 99, P at level 200, format "|==£> P") : bi_scope.
Local Lemma le_upd_unfold `{!lcGS Σ} P: Local Lemma le_upd_unfold `{!lcGS Σ} P:
(|==£> P) ⊣⊢ (|==£> P) ⊣⊢
......
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