diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index 8ff1b9d6e0343dcde158465466dc2994e79757de..31d5dbc82d8f0d2f74e1911c7d934bbcd44a0cc4 100644
--- a/stdlib/caisar.mlw
+++ b/stdlib/caisar.mlw
@@ -24,11 +24,14 @@ theory DatasetClassification
   use ieee_float.Float64
   use int.Int
   use array.Array
+  use option.Option
 
   type features = array t
   type label_ = int
   type record = (features, label_)
   type dataset = array record
+  type amplitude_record = { start: int; stop: int; step: int }
+  type amplitude = option amplitude_record
 
   constant dataset: dataset
 
@@ -69,7 +72,7 @@ theory DatasetClassificationProps
   predicate cond_robust (m: model) (d: dataset) (eps: t) =
     correct m d /\ robust m d eps
 
-  predicate meta_robust (m: model) (d: dataset) (threshold: t) (perturbation: string) (pert_path: string) (out_mode: string) (start: int) (stop: int) (step: int)
+  predicate meta_robust (m: model) (d: dataset) (threshold: t) (perturbation: string) (pert_path: string) (out_mode: string) (ampli: amplitude)
 end
 
 theory NN