revisited the inductive sum

hipsleek · May 7, 2024 · e1588ea · e1588ea
1 parent 41c90ad
commit e1588ea
Showing 1 changed file with 5 additions and 6 deletions.
diff --git a/src/demo/2_Inductive_Sum.ml b/src/demo/2_Inductive_Sum.ml
@@ -25,19 +25,18 @@ let handler n
     continue k 1
 
 
-
-(*
 let test1 () 
-(*@ ex i; Norm(i-> 10 /\ res=5, res) @*)
+(*@ ex i; Norm(i-> 15 /\ res=5, res) @*)
 = handler 5
 
 
+
 let test2 () 
-(*@ ex i; Norm(i-> 45 /\ res=10, res) @*)
+(*@ ex i; Norm(i-> 55 /\ res=10, res) @*)
 = handler 10
 
 
+
 let test3 () 
-(*@ ex i; Norm(i-> 4950 /\ res=100, res) @*)
+(*@ ex i; Norm(i-> 5050 /\ res=100, res) @*)
 = handler 100
-*)