illustration of Prop (#125)

epfl-lara · Feb 4, 2025 · c318359 · c318359
1 parent 3e326b5
commit c318359
Showing 1 changed file with 13 additions and 0 deletions.
diff --git a/tutorials/inductive-witnesses/TransitiveClosure.scala b/tutorials/inductive-witnesses/TransitiveClosure.scala
@@ -71,4 +71,17 @@ object TransitiveClosure:
   }.ensuring(proof => proof.x == x && proof.y == y)
 
 
+  final case class Prop(p: Boolean):
+    require(p)
+  val obvious = Prop(true)
+
+  def testProp = {
+    val x = 10
+    val y = 20
+    val p1 = Prop(x < y)
+  }
+  def testFunProp(x: BigInt): Prop = {
+    obvious
+  }.ensuring(_.p == (x < x + 1))
+
 end TransitiveClosure