blob: ba5939fcb123630d930bb4c373c32df728e0ef34 (
plain)
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
|
(*
Example uses of X-Symbol symbols in Coq.
See README.
Pierre Courtieu
$Id$
*)
Fixpoint toto (x:nat) {struct x} : nat := (* nat 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 nat *)
Admitted.
(* this should appear like foo'a'1_B_3 where a and B are greek *)
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.
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).
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 a b 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.
alpha lhd rhd lambda forall exists exists exist
|
