[stdlib] Rework some style.

stdlib/caisar.mlw

@@ -28,13 +28,19 @@ end
 theory SVM
   use ieee_float.Float64
   use int.Int
+
   type input_type = int -> t
   type output_type = int
-  type svm = {app : input_type -> output_type; num_input: int; num_classes: int}
 
-  predicate dist_linf (a: input_type) (b: input_type) (eps:t) (n: int) =
+  type svm = {
+    app : input_type -> output_type;
+    num_input: int;
+    num_classes: int;
+  }
+
+  predicate linfty_distance (a: input_type) (b: input_type) (eps:t) (n: int) =
     forall i. 0 <= i < n -> .- eps .< a i .- b i .< eps
 
   predicate robust_to (svm: svm) (a: input_type) (eps: t) =
-    forall b. dist_linf a b eps svm.num_input -> svm.app a = svm.app b
+    forall b. linfty_distance a b eps svm.num_input -> svm.app a = svm.app b
 end

tests/simple_ovo.t

@@ -27,12 +27,11 @@ Test verify
 
   $ caisar verify -L . --format whyml --prover=SAVer --dataset-csv=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T
-  >     use TestSVM.SVMasArray
-  >     use ieee_float.Float64
-  >     use caisar.SVM
+  >   use TestSVM.SVMasArray
+  >   use ieee_float.Float64
+  >   use caisar.SVM
   > 
-  >      goal G: forall a : input_type.
-  >      robust_to svm_apply a (8.0:t)
+  >   goal G: forall a : input_type. robust_to svm_apply a (8.0:t)
   > end
   > EOF
   <autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1