Split between code and props

leanprover · May 15, 2024 · 1b253b3 · 1b253b3
1 parent 1b87266
commit 1b253b3
Show file tree

Hide file tree

Showing 15 changed files with 21 additions and 1,492 deletions.
diff --git a/SampCert.lean b/SampCert.lean
@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean-Baptiste Tristan
 -/
 
-import SampCert.DifferentialPrivacy.ZeroConcentrated.Queries.BoundedMean.BoundedMean
+import SampCert.DifferentialPrivacy.ZeroConcentrated.Queries.BoundedMean.Code
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Composition/Composition.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Composition/Composition.lean