Skip to content

Commit 8ce013a

Browse files
committed
Typo
1 parent 0cc4580 commit 8ce013a

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

‎LeanMachineLearning/Optimization/Algorithms/Decision.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -66,4 +66,4 @@ variable (h : ∀ n (data : Iic n → α × β), μ (decision n data) ≠ 0)
6666
noncomputable def Decision : Algorithm α β where
6767
policy _ := decision_kernel μ measurableSet_decision_prod
6868
p0 := μ
69-
h_policy n := ⟨fun data => cond_isProbabilityMeasure (h n data)⟩
69+
h_policy n := ⟨fun data ↦ cond_isProbabilityMeasure (h n data)⟩

0 commit comments

Comments
 (0)