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 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84
|
(*
Example uses of Unicode Tokens symbols in Coq.
See README.
Trac this at http://proofgeneral.inf.ed.ac.uk/trac/ticket/313
Pierre Courtieu, David Aspinall.
Turn on with Proof-General → Quick Options → Display → Unicode Tokens
$Id$
*)
Module ExampleTokens.
Fixpoint toto (x:nat) {struct x} : nat := (* n a t should appear as |N *)
match x with
| O => O (* double arrow here *)
| S y => toto y (* double arrow here *)
end.
Lemma titi : forall x:nat,x=x. (* symbolique for-all and n at *)
Admitted.
(* X-Symbol: this previously appeared as foo'a'1_B_3 where a and B are greek.
Unicode Tokens: this doesn't happen because the regexp used to match
is matching on sequences limited by word.
Syntax table matters here: try (modify-syntax-entry ?\' ".")
(modify-syntax-entry ?\_ ".")
*)
Variable foo'alpha'1__beta__3 : Set.
Fixpoint pow (n m:nat) {struct n} : nat :=
match n with
| O => 0
| S p => m * pow p m
end.
Variable a b : nat.
Notation "a,{b}" := (a - b)
(at level 1, no associativity).
Notation "a^^b" := (pow a b)
(at level 1, no associativity).
Notation "a^{b}" := (pow a b)
(at level 1, no associativity, only parsing).
Variable delta:nat.
(* greek delta with a sub 1 and the same with super 1 *)
Definition delta__1 := 0.
(*Definition delta__2 := delta^^1. *)
(* Definition delta__3:= delta__2^{delta}. *)
Parameter x:nat.
(* x with a+b subscripted and then superscripted *)
(*Definition x_a_b' := x^{a+b}. *)
(*Definition x_a_b := x,{a+b}. *)
(*Definition x_a_b'' := x,{a+b}^{a*b}.*)
(* no greek letter should appear on this next line! *)
Variable philosophi : Set.
(* same here *)
Variable aalpha alphaa : Set.
(* _a where a is greek *)
Variable _alpha : Set.
(* a_ where a is greek *)
Variable alpha_ : Set.
Lemma gamma__neqn : forall n__i:nat, n__i=n__i.
Abort All.
(* Tests of things that shouldn't be
should be unicode characters: alpha lhd rhd lambda forall exists exists
shouldn't be altered: exist foral
*)
End ExampleTokens.
|