Sample examples

Author: gaetanserre

Test/Computable.lean

@@ -20,7 +20,7 @@ def logComputable {α : Type} [Lean.ToMessageData α] (prog : RandPCG IO α) : C
 
 attribute [computable] sumTwo
 
-run_cmd do logComputable sumTwoComputable
+run_cmd logComputable sumTwoComputable
 
 @[computable]
 noncomputable
@@ -31,20 +31,20 @@ def unfoldSumTwo : MeasureTheory.Measure ℝ := rdo
 
 attribute [computable] centred
 
-run_cmd do logComputable (centredComputable 20)
+run_cmd logComputable (centredComputable 20)
 
 attribute [computable] branchOn
 
 run_cmd do logComputable (branchOnComputable 20)
 
-run_cmd do logComputable (branchOnComputable (-1))
+run_cmd logComputable (branchOnComputable (-1))
 
 attribute [computable] fairCoin
 
-run_cmd do logComputable (fairCoinComputable)
+run_cmd logComputable (fairCoinComputable)
 
 attribute [computable] Bind.twoCoins
 
-run_cmd do logComputable (Bind.twoCoinsComputable)
+run_cmd logComputable (Bind.twoCoinsComputable)
 
 end Test.Computable

Test/Sample.lean

@@ -0,0 +1,31 @@
+module
+
+public import RandomDo
+
+set_option linter.style.header false
+
+open NumLean IO Lean
+
+run_cmd do
+  let x ← rand 0 1000
+  logInfo m!"Random number between 0 and 1000: {x}"
+
+run_cmd do
+  let x ← (runRandPCG <| randInt 1000 : IO Int)
+  logInfo m!"Random number between 0 and 1000 (PCG): {x}"
+
+run_cmd do
+  let x ← (runRandPCG <| normal 10 2 : IO Float)
+  logInfo m!"{x}"
+
+run_cmd do
+  let x ← (runRandPCG <| exponential 10 : IO Float)
+  logInfo m!"{x}"
+
+run_cmd do
+  let x ← (runRandPCG <| binomial 10 0.5 : IO Nat)
+  logInfo m!"{x}"
+
+run_cmd do
+  let x ← (runRandPCG <| bernoulli 0.5 : IO Nat)
+  logInfo m!"{x}"