More abstract composition

leanprover · May 20, 2024 · 83ddf1e · 83ddf1e
1 parent 979d243
commit 83ddf1e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Composition/Code.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Composition/Code.lean
@@ -10,7 +10,7 @@ noncomputable section
 
 namespace SLang
 
-def Compose (nq1 nq2 : List T → SLang ℤ) (l : List T) : SLang (ℤ × ℤ) := do
+def Compose (nq1 nq2 : List T → SLang U) (l : List T) : SLang (U × U) := do
   let A ← nq1 l
   let B ← nq2 l
   return (A,B)