From e7bcdb0e11b7af04cc4f6e86203d32cdb9ec3fe8 Mon Sep 17 00:00:00 2001 From: lecopivo Date: Fri, 18 Oct 2024 14:03:42 +0200 Subject: [PATCH] fix test --- test/probability/rand_with_trace.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/test/probability/rand_with_trace.lean b/test/probability/rand_with_trace.lean index 1b0c09f9..e7c28c61 100644 --- 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