From 801e65f796b46caff7e1248db442102e0f943f44 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 16 Apr 2004 11:32:42 +0000
Subject: added an example fils for coq x-symbols.

---
 coq/example-x-symbols.v | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)
 create mode 100644 coq/example-x-symbols.v

diff --git a/coq/example-x-symbols.v b/coq/example-x-symbols.v
new file mode 100644
index 00000000..c3bee71e
--- /dev/null
+++ b/coq/example-x-symbols.v
@@ -0,0 +1,37 @@
+(* Grammar for symbols:
+  a symbol is encoded only if 
+   - preceded by _ or some space or some symbol
+  **and**
+   - followed by _ or some space or some symbol
+
+  Grammar for sub/superscript: 
+
+   - a double _ introduces a subscript that ends at the first space
+   - a double ^ introduces a superscript that ends at the first space
+  
+   - a _ followed by { introduces a subscript
+     expression that ends at the first }
+   - a ^ followed by { introduces a superscript
+     expression that ends at the first }
+ *)
+
+
+
+foo_alpha_1_beta_3  (* this should appear like foo_a_1_B_3 where a and B are greek *)
+delta__1 delta^^1          (* greek delta with a sub 1 and the same with super 1 *)
+x_{a+b} x^{a+b}         (* x with a+b subscripted and then superscripted *)
+philosophi   (* no greek letter should appear on this line *)
+aalpha alphaa (* no greek letter *)
+_alpha           (* _a where a is greek *)
+alpha_           (* a_ where a is greek *)
+
+
+
+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 *)
+ 
\ No newline at end of file
-- 
cgit v1.2.3