notation.v 1.75 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From stdpp Require Export strings.
2
From iris.proofmode Require Import coq_tactics environments.
3
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
4

Ralf Jung's avatar
Ralf Jung committed
5
Declare Scope proof_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
Delimit Scope proof_scope with env.
7
Arguments Envs _ _%proof_scope _%proof_scope _.
Robbert Krebbers's avatar
Robbert Krebbers committed
8
Arguments Enil {_}.
Robbert Krebbers's avatar
Robbert Krebbers committed
9
Arguments Esnoc {_} _%proof_scope _%string _%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
10

Ralf Jung's avatar
Ralf Jung committed
11
Notation "" := Enil (only printing) : proof_scope.
12
Notation "Γ H : P" := (Esnoc Γ (INamed H) P%I)
Robbert Krebbers's avatar
Robbert Krebbers committed
13
  (at level 1, P at level 200,
14
   left associativity, format "Γ H  :  '[' P ']' '//'", only printing) : proof_scope.
15
Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P%I)
16
  (at level 1, P at level 200,
17
   left associativity, format "Γ '_'  :  '[' P ']' '//'", only printing) : proof_scope.
18

19
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
20
  (envs_entails (Envs Γ Δ _) Q%I)
Robbert Krebbers's avatar
Robbert Krebbers committed
21
  (at level 1, Q at level 200, left associativity,
Ralf Jung's avatar
Ralf Jung committed
22
  format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
Robbert Krebbers's avatar
Robbert Krebbers committed
23
  stdpp_scope.
24
Notation "Δ '--------------------------------------' ∗ Q" :=
25
  (envs_entails (Envs Enil Δ _) Q%I)
Robbert Krebbers's avatar
Robbert Krebbers committed
26
  (at level 1, Q at level 200, left associativity,
Robbert Krebbers's avatar
Robbert Krebbers committed
27
  format "Δ '--------------------------------------' ∗ '//' Q '//'", only printing) : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
Notation "Γ '--------------------------------------' □ Q" :=
29
  (envs_entails (Envs Γ Enil _) Q%I)
Robbert Krebbers's avatar
Robbert Krebbers committed
30
  (at level 1, Q at level 200, left associativity,
Robbert Krebbers's avatar
Robbert Krebbers committed
31
  format "Γ '--------------------------------------' □ '//' Q '//'", only printing)  : stdpp_scope.
32
Notation "'--------------------------------------' ∗ Q" := (envs_entails (Envs Enil Enil _) Q%I)
Robbert Krebbers's avatar
Robbert Krebbers committed
33
  (at level 1, Q at level 200, format "'--------------------------------------' ∗ '//' Q '//'", only printing) : stdpp_scope.