diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw index 4010d785523625f029b1f16fa94a74da03e07074..5f5f3d336f05ff25b3d2d344be8692adac6d8e0d 100644 --- a/stdlib/caisar.mlw +++ b/stdlib/caisar.mlw @@ -33,14 +33,14 @@ theory SVM type output_type = int type svm = { - app : input_type -> output_type; - num_input: int; - num_classes: int; + apply : input_type -> output_type; + nb_inputs : int; + nb_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. linfty_distance a b eps svm.num_input -> svm.app a = svm.app b + forall b. linfty_distance a b eps svm.nb_inputs -> svm.apply a = svm.apply b end