Commit b19439bf authored by Dan Frumin's avatar Dan Frumin

Improve the notation

parent 4748876b
......@@ -209,7 +209,7 @@ Section Stack_refinement.
unfold FG_read_iter, CG_snap_iter. unlock.
simpl_subst/=.
iApply bin_log_related_arrow; eauto.
iAlways. iIntros ([f1 f2]) "#Hff".
iAlways. iIntros ([f1 f2]) "#Hff /=".
rel_rec_r.
rel_rec_l.
Transparent FG_iter CG_iter. unlock FG_iter CG_iter.
......@@ -298,8 +298,7 @@ Section Stack_refinement.
by iApply "IH".
+ clear.
iClear "IH Histk HLK_tail HLK HLK' Hτ".
iApply related_ret.
iApply "Hff".
iApply (related_ret with "[Hff]"). done.
Qed.
End Stack_refinement.
......
......@@ -398,11 +398,13 @@ Section bin_log_def.
End bin_log_def.
Notation "'{' E1 ',' E2 ';' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
(bin_log_related E1 E2 Δ Γ e%E e'%E τ) (at level 74, E1,E2, e, e', τ at next level).
(bin_log_related E1 E2 Δ Γ e%E e'%E τ) (at level 74, E1,E2, e, e', τ at next level,
format "'{' E1 ',' E2 ';' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ").
Notation "'{' E1 ',' E2 ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
( Δ, bin_log_related E1 E2 Δ Γ e%E e'%E τ)%I (at level 74, E1,E2, e, e', τ at next level).
Notation "Γ ⊨ e '≤log≤' e' : τ" :=
( Δ, bin_log_related Δ Γ e%E e'%E τ)%I (at level 74, e, e', τ at next level).
( Δ, bin_log_related Δ Γ e%E e'%E τ)%I (at level 74, e, e', τ at next level,
format "Γ ⊨ e '≤log≤' e' : τ").
Section monadic.
Context `{logrelG Σ}.
......
......@@ -19,12 +19,7 @@ Coercion BNamed : string >-> binder.
Notation "<>" := BAnon : binder_scope.
Notation Lam x e := (Rec BAnon x e).
Notation Let x e1 e2 := (App (Lam x e2) e1).
Notation Seq e1 e2 := (Let BAnon e1 e2).
Notation LamV x e := (RecV BAnon x e).
Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
Notation SeqCtx e2 := (LetCtx BAnon e2).
Notation Skip := (Seq tt tt).
(* No scope for the values, does not conflict and scope is often not inferred
properly. *)
......@@ -78,10 +73,6 @@ Notation "λ: x , e" := (locked (LamV x%bind e%E))
(at level 102, x at level 1, e at level 200) : val_scope.
Notation "λ: x y .. z , e" := (locked (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. )))
(at level 102, x, y, z at level 1, e at level 200) : val_scope.
Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
(at level 100, e2 at level 200, format "e1 ;; e2") : expr_scope.
Notation "e1 ;; e2" := (LamV BAnon e2%E e1%E)
(at level 100, e2 at level 200, format "e1 ;; e2") : val_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
(at level 200, e1, e2, e3 at level 200) : expr_scope.
......@@ -93,7 +84,9 @@ Notation "'Λ:' e" := (TLam e%E)
Notation "'Λ:' e" := (TLamV e%E)
(at level 102, e at level 200) : val_scope.
Notation "'let:' x := e1 'in' e2" := (Let x%bind e1%E e2%E)
Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%E e1%E)
(at level 102, x at level 1, e1, e2 at level 200,
format "'[' '[hv' 'let:' x := '[' e1 ']' 'in' ']' '/' e2 ']'") : expr_scope.
Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
(at level 100, e2 at level 200, format "e1 ;; e2") : expr_scope.
......@@ -254,7 +254,7 @@ Section properties.
(Hclosed1 : Closed e1)
(Hclosed2 : Closed e2) :
({E,E;Δ;Γ} fill K e1 log t : τ)
{E,E;Δ;Γ} fill K (If (# true) e1 e2) log t : τ.
{E,E;Δ;Γ} fill K (If true e1 e2) log t : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros.
......
Markdown is supported
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