remove biginteger reference in uniformintervalsample32

dafny-lang · Mar 12, 2024 · 88dd436 · 88dd436
1 parent b2a5f41
commit 88dd436
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/Distributions/Uniform/Interface.dfy b/src/Distributions/Uniform/Interface.dfy
@@ -47,10 +47,10 @@ module Uniform.Interface {
       ensures a <= u < b
       ensures Model.IntervalSample(a as int, b as int)(old(s)) == Monad.Result(u as int, s)
     {
-      var v := UniformSample32((b as int - a as int) as pos32);
+      var v := UniformSample32(b-a);
       assert Model.Sample(b as int - a as int)(old(s)) == Monad.Result(v as nat, s);
       assert Model.IntervalSample(a as int, b as int)(old(s)) == Monad.Result(a as int + v as int, s);
-      u := a + (v as int32);
+      u := a + v;
     }
 
   }