From 5d64d1f3bfb7694cbb6b0e7f4f7ba7e93b2cbf2a Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 11 Aug 2010 16:58:48 +0000 Subject: Try to fix processing of this file --- coq/example-tokens.v | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'coq/example-tokens.v') diff --git a/coq/example-tokens.v b/coq/example-tokens.v index 773c326c..b6ea2a29 100644 --- a/coq/example-tokens.v +++ b/coq/example-tokens.v @@ -30,6 +30,8 @@ Fixpoint pow (n m:nat) {struct n} : nat := | S p => m * pow p m end. +Variable a b : nat. + Notation "a,{b}" := (a - b) (at level 1, no associativity). @@ -37,15 +39,15 @@ Notation "a^^b" := (pow a b) (at level 1, no associativity). Notation "a^{b}" := (pow a b) - (at level 1, no associativity). + (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}. +Definition delta__1 := 0. +Definition delta__2 := delta^^1. +Definition delta__3:= delta__2^{delta}. Parameter a b x:nat. @@ -70,4 +72,7 @@ Variable alpha_ : Set. Lemma gamma__neqn : forall n__i:nat, n__i=n__i. -alpha lhd rhd lambda forall exists exists exist foral +(* Tests of things that shouldn't be +should be unicode characters: alpha lhd rhd lambda forall exists exists +shouldn't be altered: exist foral +*) -- cgit v1.2.3