NIT

logsem · Nov 29, 2024 · 3d4c1db · 3d4c1db
1 parent a6dc977
commit 3d4c1db
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/prob/distribution.v b/theories/prob/distribution.v
@@ -2402,7 +2402,7 @@ Section laplace.
         * apply ex_seriesC_scal_l, ex_seriesC_laplace_f_nat.
   Qed.
 
-  Program Definition laplace' ε : distr (Z) :=
+  Program Definition laplace ε : distr (Z) :=
     MkDistr (λ z, laplace_f ε z / SeriesC (λ z, laplace_f ε z)) _ _ _.
   Next Obligation.
     intros. rewrite /laplace_f.