UTF8Module

Pierre Letouzey edited this page Oct 13, 2017 · 18 revisions

This file is created from scratch. Feel free to enlarge/shorten/modify it. It is tried that the levels given here are consistent with the output of Print Grammar constr command. Yet some levels are chosen arbitrarily, for the apparent lack of a better alternative at the time of the creation. -- MiladNiqui 2005-05-31 16:53:09

(* Notation " A ⇒ B " := (A => B) (at level 90, right associativity) : type_scope. *)
Notation " A → B " := (A -> B) (at level 90, right associativity) : type_scope.
(* Notation " A ← B " := (A <- B) (at level 90, right associativity) : type_scope. *)
Notation " ∀ x , B  " := (forall x:_, B ) (at level 200, x at level 0, no associativity) : type_scope.
Notation " ∀ x y , B  " := (forall (x:_) (y:_), B ) (at level 200, x at level 0, y at level 0, no associativity) : type_scope.
Notation " ∀ x y z , B  " := (forall (x:_) (y:_) (z:_), B ) (at level 200, x at level 0, y at level 0, z at level 0, no associativity) : type_scope.
Notation " ∀ x y z t , B  " := (forall (x:_) (y:_) (z:_) (t:_), B ) (at level 200, x at level 0, y at level 0, z at level 0, t at level 0, no associativity) : type_scope.
Notation " ∀ x y z t u , B  " := (forall (x:_) (y:_) (z:_) (t:_) (u:_), B ) (at level 200, x at level 0, y at level 0, z at level 0, t at level 0, u at level 0, no associativity) : type_scope.
Notation " ∀ x : A , B  " := (forall x:A, B ) (at level 200, x at level 0, no associativity) : type_scope.
Notation " ∀ ( x : A1 )  ( y : A2 ) , B  " := (forall (x:A1) (y:A2), B ) (at level 200, x at level 0, y at level 0, no associativity) : type_scope.
Notation " ∀ x ( y : A2 ) , B  " := (forall (x:_) (y:A2), B ) (at level 200, x at level 0, y at level 0, no associativity) : type_scope.
Notation " ¬ x " := (not  x) (at level 75, right associativity) : type_scope.
Notation " A × B " := (A * B) (at level 40, left associativity) : type_scope.
Notation " A ≠ B " := (A <> B) (at level 70, no associativity) : type_scope.
Notation " A ≠ B :> T " := (A <> B :> T) (at level 70, no associativity) : type_scope.
Notation " A ≤ B " := (A <= B) (at level 70, no associativity) : type_scope.
Notation " A ≥ B " := (A >= B) (at level 70, no associativity) : type_scope.
Notation " A ∧ B " := (A /\ B) (at level 80, right associativity) : type_scope.
Notation " A ⇔ B " := (A <-> B) (at level 95, right associativity) : type_scope.
Notation " ⊥ " := (False) : type_scope.
Notation " ⊤ " := (True) : type_scope.
Notation " A ∨ B " := (A \/ B) (at level 85, right associativity) : type_scope.
Notation " ∃ x , B  " := (ex (fun x:_=>B) ) (at level 0, x at level 99, no associativity) : type_scope.
Notation " ∃ x : A , B  " := (ex (fun x:A=>B) ) (at level 0, x at level 99, no associativity) : type_scope.
Notation " ∃! x , B  " := (ex (unique (fun x => B))) (at level 200, x ident, right associativity) : type_scope.
Notation " ∃! x : A , B  " := (ex (unique (fun x:A => B))) (at level 200, x ident, right associativity) : type_scope.
Notation " 'ℕ' " := nat : type_scope.
(* Notation  "'λ' x : T , y" := (fun x:T => y) (at level 1, x,T,y at level 10). *)
Notation  "x : T ⟼ y" := (fun x:T => y) (at level 1, x,T,y at level 10).
(* Notation  "'λ' x := T , y" := ([x:=T] y) (at level 1, x,T,y at level 10). *)
(* Notation " 'ℤ' " := Int : type_scope.
Notation " 'ℤ'⁺ " := positive : type_scope.
Notation " 'ℚ' " := Q : type_scope.
Notation " 'ℝ' " := R : type_scope.
Notation " 'ℝ' ⁺ " := posreal : type_scope.
Notation " 'ℝ' ⁻ " := negreal : type_scope. *)

utf8.v

Usage

This file (and all the files based on the notation defined in this file) should be saved with the charset encoding UTF-8, otherwise you won't be able to compile it with coqc. In order to ensure this in CoqIde you should go to

Edit -> Preferences -> Files

and set File charset encoding to UTF-8. (This is also explained in Section 14.8.3 of the Reference Manual.)

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.