Merge branch 'main' into forFix

Author: gaetanserre

.github/workflows/build.yml

@@ -47,7 +47,7 @@ jobs:
           # the single fetched commit.
           fetch-depth: 0 # Fetch all history for all branches and tags
 
-      - name: Build and lint project
+      - name: Build, lint and test project
         uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
         with:
           build: true

RandomDo/Measurable.lean

@@ -117,7 +117,8 @@ def Vector.measurableEquivTuple {n : ℕ} : Vector α n ≃ᵐ (Fin n → α) wh
     ext
     simp
 
-instance : MeasurableSpace (Option α) := MeasurableSpace.map some inferInstance
+instance instMeasurableSpaceOption : MeasurableSpace (Option α) :=
+  MeasurableSpace.map some inferInstance
 
 theorem measurableSet_option_iff {s : Set (Option α)} :
     MeasurableSet s ↔ MeasurableSet (some ⁻¹' s) := Iff.rfl

RandomDo/Monad/ForInInstances.lean

@@ -20,13 +20,13 @@ section MeasurableSpace
 
 variable {α : Type*} [MeasurableSpace α]
 
-instance : MeasurableSpace (List α) :=
+instance instMeasurableSpaceList : MeasurableSpace (List α) :=
   MeasurableSpace.comap List.equivSigmaTuple inferInstance
 
-instance : MeasurableSpace (Array α) :=
+instance instMeasurableSpaceArray : MeasurableSpace (Array α) :=
   MeasurableSpace.comap Array.toList inferInstance
 
-instance {n : ℕ} : MeasurableSpace (Vector α n) :=
+instance instMeasurableSpaceVector {n : ℕ} : MeasurableSpace (Vector α n) :=
   MeasurableSpace.comap Vector.toArray inferInstance
 
 instance instMeasurableSpaceSubarray : MeasurableSpace (Subarray α) :=
@@ -59,7 +59,7 @@ section Array
   {β : Type u} [mβ : MeasurableSpace β]
   (as : Array α) (b : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
   let sz := as.usize
-  let rec @[specialize] loop (i : USize) (b : β) : m β := rdo
+  let rec @[specialize, nolint docBlame] loop (i : USize) (b : β) : m β := rdo
     if i < sz then
       let a := as.uget i lcProof
       match (← f a lcProof b) with
@@ -74,7 +74,7 @@ section Array
 protected def Array.measurableSpaceForIn' [MeasurableSpaceMonad m]
   {β : Type u} [mβ : MeasurableSpace β]
   (as : Array α) (b : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
-  let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := rdo
+  let rec @[nolint docBlame] loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := rdo
     match i, h with
     | 0,   _ => mPure b
     | i+1, h =>
@@ -104,7 +104,7 @@ variable {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [Ring α]
 protected def List.measurableSpaceForIn' [MeasurableSpaceMonad m]
     {β : Type u} [mβ : MeasurableSpace β] (as : @& List α) (init : β)
     (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
-  let rec @[specialize]
+  let rec @[specialize, nolint docBlame]
     loop : (as' : @& List α) → (b : β) → Exists (fun bs => bs ++ as' = as) → m β
       | [], b, _    => mPure b
       | a::as', b, h => rdo

RandomDo/Monad/Instances.lean

@@ -57,6 +57,8 @@ open Function
 /-- A monad for random number generation. -/
 structure RandomM (Ω : Type w) [MeasurableSpace Ω] (P : Measure Ω)
     (α : Type u) [MeasurableSpace α] where
+  /-- Draws a value from a state of the source of randomness, and hands back the state left for the
+  next draw. -/
   sample : Ω → α × Ω
   measurePreserving : MeasurePreserving sample P ((Measure.map (Prod.fst ∘ sample) P).prod P)
 

RandomDo/Monad/MeasurableSpace.lean

@@ -142,8 +142,6 @@ variable {f : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpac
     g₁ <$>ₘ g₀ <$>ₘ x = (fun a => g₁ (g₀ a)) <$>ₘ x :=
   (comp_mMap x hg₀ hg₁).symm
 
-@[simp] theorem mMap_unit {a : f PUnit} : (fun _ => PUnit.unit) <$>ₘ a = a := by simp
-
 open MeasurableSpaceBind MeasurableSpacePure MeasurableSpaceFunctor
 
 /-- A `MeasurableSpaceMonad` satisfies the measurable space monad laws. -/

Test/Common.lean

@@ -1,6 +1,7 @@
 module
 
 public import RandomDo
+public import Mathlib.Probability.Distributions.Bernoulli
 
 set_option linter.style.header false
 

lakefile.toml

@@ -1,6 +1,7 @@
 name = "RandomDo"
-defaultTargets = ["RandomDo", "Test"]
+defaultTargets = ["RandomDo"]
 lintDriver = "batteries/runLinter"
+testDriver = "Test"
 
 [leanOptions]
 pp.unicode.fun = true