1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i $Id$ i*)
Require Export Logic.
(** Symbolic notations for things in [Logic.v] *)
Notation "< P , Q > { p , q }" := (conj P Q p q) (P annot, at level 1).
Notation "~ x" := (not x) (at level 5, right associativity).
Notation "x = y" := (eq ? x y) (at level 5, no associativity).
Infix RIGHTA 6 "/\\" and.
Infix RIGHTA 7 "\\/" or.
Infix RIGHTA 8 "<->" iff.
Notation "'IF' c1 'then' c2 'else' c3" := (IF c1 c2 c3)
(at level 1, c1, c2, c3 at level 8).
(* Order is important to give printing priority to fully typed ALL and EX *)
Notation All := (all ?).
Notation "'ALL' x | p" := (all ? [x]p) (at level 10, p at level 8).
Notation "'ALL' x : t | p" := (all t [x:t]p) (at level 10, p at level 8).
Notation Ex := (ex ?).
Notation "'EX' x | p" := (ex ? [x]p) (at level 10, p at level 8).
Notation "'EX' x : t | p" := (ex t [x:t]p) (at level 10, p at level 8).
Notation Ex2 := (ex2 ?).
Notation "'EX' x | p & q" := (ex2 ? [x]p [x]q)
(at level 10, p, q at level 8).
Notation "'EX' x : t | p & q" := (ex2 t [x:t]p [x:t]q)
(at level 10, p, q at level 8).
(** Parsing only of things in [Logic.v] *)
Notation "< A > 'All' ( P )" := (all A P) (A annot, at level 1, only parsing).
Notation "< A > x = y" := (eq A x y) (A annot, at level 1, x at level 0, only parsing).
|
