fix test

lecopivo · Oct 18, 2024 · e7bcdb0 · e7bcdb0
1 parent 796104c
commit e7bcdb0
Showing 1 changed file with 1 addition and 4 deletions.
diff --git a/test/probability/rand_with_trace.lean b/test/probability/rand_with_trace.lean
@@ -1,4 +1,5 @@
 import SciLean.Probability.RandWithTrace
+import SciLean.Analysis.Scalar.FloatAsReal
 
 open SciLean Rand MeasureTheory
 
@@ -39,10 +40,6 @@ info: tt :
 #check tt
 
 
-instance (n:Nat) [MeasureSpace X] : MeasureSpace {a : Array X // a.size = n} := sorry
-instance (n:Nat) [MeasureSpace X] : MeasureSpace (ArrayN X n) := sorry
-
-
 /--
 info: fun x =>
   pdf Float