wip

winitzki · Oct 14, 2024 · 22baef5 · 22baef5
1 parent d6aa041
commit 22baef5
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/tutorial/Float/add.dhall b/tutorial/Float/add.dhall
@@ -542,7 +542,7 @@ let _ = assert : checkAddShow -12345678 -8 +123 -2 5 "+1.10655"
 
 let _ = assert : checkAddShow -12345678 -8 +123 -2 9 "+1.10654322"
 
-in  { --Float/add,
+in  { Float/add,
       addOrSubtractUnsignedAIsGreater
     , subtractUnsignedAMinusB
     , addUnsignedBothNonzero

diff --git a/tutorial/Float/compare.dhall b/tutorial/Float/compare.dhall
@@ -216,13 +216,13 @@ let zeroTorsor = { x = 0, y = 0 }
 
 let computeTorsor
     : Integer → TorsorType
-    =    {-
+    =
     stop.reduce_growth
         Integer
         stop.predicate_Integer
         TorsorType
         zeroTorsor
-            -}
+
         ( λ(i : Integer) →
             if    Integer/positive i
             then  { x = Integer/clamp i, y = 0 }
@@ -233,13 +233,13 @@ let computeTorsorForBothNonzero
     -- We define "torsor(a, b)" as any pair of `Natural` numbers (x, y) such that floor(log_10(a)) - floor(log_10(b)) = x - y.
     : Pair Float Float → TorsorType
     =
-    {-
+
     stop.reduce_growth
         (Pair Float Float)
         (λ(pair : Pair Float Float) → stop.predicate_Natural pair._1.mantissa)
         TorsorType
         zeroTorsor
-      -}
+
         ( λ(pair : Pair Float Float) →
             let a = pair._1