notation.v 1.46 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.proofmode Require Import coq_tactics environments.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From fast_string Require Export fast_string_lib.
3
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
4
5
6
7
8
9

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

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