Commit 6d021c73 authored by Robbert Krebbers's avatar Robbert Krebbers

Put notations for proofmode environment manipulation into a module.

parent f774d316
......@@ -3,13 +3,7 @@ From iris.algebra Require Import upred_big_op upred_tactics.
From iris.proofmode Require Export environments classes.
From iris.prelude Require Import stringmap hlist.
Import uPred.
Local Notation "Γ !! j" := (env_lookup j Γ).
Local Notation "x ← y ; z" := (match y with Some x => z | None => None end).
Local Notation "' ( x1 , x2 ) ← y ; z" :=
(match y with Some (x1,x2) => z | None => None end).
Local Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
(match y with Some (x1,x2,x3) => z | None => None end).
Import env_notations.
Record envs (M : ucmraT) :=
Envs { env_persistent : env (uPred M); env_spatial : env (uPred M) }.
......
......@@ -10,18 +10,21 @@ Arguments Esnoc {_} _ _%string _.
Instance: Params (@Enil) 1.
Instance: Params (@Esnoc) 1.
Local Notation "x ← y ; z" := (match y with Some x => z | None => None end).
Local Notation "' ( x1 , x2 ) ← y ; z" :=
(match y with Some (x1,x2) => z | None => None end).
Local Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
(match y with Some (x1,x2,x3) => z | None => None end).
Fixpoint env_lookup {A} (i : string) (Γ : env A) : option A :=
match Γ with
| Enil => None
| Esnoc Γ j x => if decide (i = j) then Some x else env_lookup i Γ
end.
Local Notation "Γ !! j" := (env_lookup j Γ).
Module env_notations.
Notation "x ← y ; z" := (match y with Some x => z | None => None end).
Notation "' ( x1 , x2 ) ← y ; z" :=
(match y with Some (x1,x2) => z | None => None end).
Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
(match y with Some (x1,x2,x3) => z | None => None end).
Notation "Γ !! j" := (env_lookup j Γ).
End env_notations.
Import env_notations.
Inductive env_wf {A} : env A Prop :=
| Enil_wf : env_wf Enil
......
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