From 30fefc19f0aba774010f3349273cf5dbf8dd1b42 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 2 Sep 2022 10:23:48 +0200
Subject: [PATCH] [stdlib] Rework svm type in stdlib to be coherent with type
naming in code.
---
stdlib/caisar.mlw | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index 4010d78..5f5f3d3 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
--
GitLab