notation.v 1.35 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6 7 8 9
From iris.proofmode Require Import coq_tactics environments.
From iris.prelude Require Export strings.

Delimit Scope proof_scope with env.
Arguments Envs _ _%proof_scope _%proof_scope.
Arguments Enil {_}.
Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope.

Notation "​" := Enil (format "​") : proof_scope.
10
Notation "Γ ​ H : P" := (Esnoc Γ H P)
Robbert Krebbers's avatar
Robbert Krebbers committed
11
  (at level 1, P at level 200,
12
   left associativity, format "Γ ​ H  :  P '//'") : proof_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
13 14 15
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ★ Q" :=
  (of_envs (Envs Γ Δ)  Q%I)
  (at level 1, Q at level 200, left associativity,
16
  format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ★ '//' Q '//'") :
Robbert Krebbers's avatar
Robbert Krebbers committed
17 18 19 20
  C_scope.
Notation "Δ '--------------------------------------' ★ Q" :=
  (of_envs (Envs Enil Δ)  Q%I)
  (at level 1, Q at level 200, left associativity,
21
  format "Δ '--------------------------------------' ★ '//' Q '//'") : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
22 23 24
Notation "Γ '--------------------------------------' □ Q" :=
  (of_envs (Envs Γ Enil)  Q%I)
  (at level 1, Q at level 200, left associativity,
25
  format "Γ '--------------------------------------' □ '//' Q '//'")  : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
Notation "​​ Q" := (of_envs (Envs Enil Enil)  Q%I)
27
  (at level 1, Q at level 200, format "​​ Q") : C_scope.