test.why 834 Bytes
 Jean-Christophe Filliâtre committed Feb 09, 2010 1 2 3 `````` (* test file *) `````` 4 5 ``````theory A type t `````` Jean-Christophe Filliâtre committed Feb 25, 2010 6 `````` logic c : t `````` 7 8 9 ``````end theory B `````` Jean-Christophe Filliâtre committed Feb 25, 2010 10 11 12 13 14 `````` namespace S type t end logic d : S.t logic f : S.t -> S.t logic p : S.t -> prop axiom Ax : forall x:S.t. p(x) or p(f(x)) `````` 15 16 ``````end `````` Jean-Christophe Filliâtre committed Feb 18, 2010 17 ``````theory Int `````` Jean-Christophe Filliâtre committed Feb 17, 2010 18 19 20 `````` type int end `````` Jean-Christophe Filliâtre committed Feb 18, 2010 21 ``````theory Eq `````` Jean-Christophe Filliâtre committed Feb 15, 2010 22 `````` `````` Francois Bobot committed Feb 22, 2010 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 `````` logic eq : 'a, 'a -> prop (* This part is just a definition of the equality *) (* This theory define eq but of course these axioms should not be send to provers *) axiom refl : forall x:'a. eq(x,x) axiom sym : forall x,y:'a. eq(x,y) -> eq(y,x) axiom trans : forall x,y,z:'a. eq(x,y) -> eq(y,z) -> eq(x,z) (* This one can't be written in first order logic. *) type t type u logic f : t -> u axiom congru : forall x,y:t. eq(x,y) -> eq(f(x),f(y)) `````` Jean-Christophe Filliâtre committed Feb 15, 2010 38 `````` `````` Jean-Christophe Filliâtre committed Feb 17, 2010 39 ``````end `````` Jean-Christophe Filliâtre committed Feb 15, 2010 40 `````` `````` Jean-Christophe Filliâtre committed Feb 25, 2010 41 ``````(* `````` Jean-Christophe Filliâtre committed Feb 19, 2010 42 ``````theory Test `````` Jean-Christophe Filliâtre committed Feb 17, 2010 43 `````` `````` 44 45 `````` use Eq use import L : List `````` Jean-Christophe Filliâtre committed Feb 21, 2010 46 `````` axiom a : forall x : 'a. not Eq.eq(nil, cons(nil, nil)) `````` Jean-Christophe Filliâtre committed Feb 17, 2010 47 `````` `````` Jean-Christophe Filliâtre committed Feb 25, 2010 48 49 ``````end *)``````