test-claude.why 1.26 KB
 MARCHE Claude committed Sep 17, 2010 1 ``````theory TestInt `````` MARCHE Claude committed Apr 18, 2010 2 3 4 `````` use import int.Int `````` MARCHE Claude committed Sep 08, 2010 5 6 `````` goal Test0 : true `````` MARCHE Claude committed Oct 26, 2010 7 `````` goal Test0_5 : true -> false `````` MARCHE Claude committed Sep 08, 2010 8 `````` `````` MARCHE Claude committed Apr 18, 2010 9 10 11 12 `````` goal Test1: 2+2 = 4 goal Test2: forall x:int. x*x >= 0 `````` MARCHE Claude committed Sep 01, 2010 13 `````` goal Test3: 1<>0 `````` MARCHE Claude committed Sep 09, 2010 14 15 16 17 18 `````` goal Test4: 1=2 -> 3=4 goal Test5: forall x:int. x <> 0 -> x*x > 0 `````` MARCHE Claude committed Sep 23, 2010 19 20 21 `````` goal Test6: 2+3 = 5 and (forall x:int. x*x >= 0) goal Test7: 0 = 1 /\ 2 = 3 /\ 4 = 5 /\ 6 = 7 `````` MARCHE Claude committed Oct 26, 2010 22 23 24 25 `````` (* goal Test8: 3+3=7 *) `````` MARCHE Claude committed Sep 16, 2010 26 `````` `````` MARCHE Claude committed Sep 17, 2010 27 28 29 30 31 ``````end theory TestDiv use import int.Int `````` MARCHE Claude committed Sep 16, 2010 32 33 34 35 36 37 38 39 40 41 42 43 `````` use int.EuclideanDivision goal EDiv1: EuclideanDivision.div 1 2 = 0 goal EDiv2: EuclideanDivision.div (-1) 2 = -1 use int.ComputerDivision goal CDiv1: ComputerDivision.div 1 2 = 0 goal CDiv2: ComputerDivision.div (-1) 2 = 0 `````` MARCHE Claude committed Sep 17, 2010 44 45 ``````end `````` MARCHE Claude committed Oct 08, 2010 46 `````` `````` MARCHE Claude committed Sep 17, 2010 47 48 ``````theory TestReal `````` MARCHE Claude committed Sep 09, 2010 49 `````` use import real.Real `````` MARCHE Claude committed Sep 16, 2010 50 51 52 `````` goal Real1: forall x:real. x <> 0.0 -> x*x <> 0.0 `````` MARCHE Claude committed Sep 09, 2010 53 54 `````` use import real.Abs `````` MARCHE Claude committed Oct 26, 2010 55 `````` goal RealAbs1: forall x:real. 100.0 >= abs x >= 1.0 -> x*x >= 1.0 `````` MARCHE Claude committed Sep 09, 2010 56 `````` `````` MARCHE Claude committed Sep 17, 2010 57 58 59 60 ``````end theory TestFloat `````` MARCHE Claude committed Sep 15, 2010 61 62 63 64 65 `````` use import floating_point.Rounding use floating_point.Single lemma Round_single_01: Single.round NearestTiesToEven 0.1 = 0x0.199999Ap0 `````` MARCHE Claude committed Apr 18, 2010 66 67 ``````end `````` MARCHE Claude committed Sep 23, 2010 68 `````` `````` MARCHE Claude committed Oct 08, 2010 69 `````` `````` MARCHE Claude committed Sep 23, 2010 70 71 72 73 74 75 76 ``````theory TestList use import int.Int use import list.List logic x : list int `````` MARCHE Claude committed Oct 26, 2010 77 ``````(* `````` MARCHE Claude committed Sep 23, 2010 78 79 80 81 82 83 `````` goal Test1: match x with | Nil -> 1 = 0 /\ 2 = 3 | Cons _ Nil -> 4 = 5 and 6 = 7 | Cons _ _ -> 8 = 9 /\ 10 = 11 end `````` MARCHE Claude committed Oct 26, 2010 84 ``````*) `````` MARCHE Claude committed Sep 23, 2010 85 `````` `````` MARCHE Claude committed Sep 28, 2010 86 ``end ``