From c318359ae26d1339ea57802fbac478b0456151e8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Viktor=20Kun=C4=8Dak?= <vkuncak@users.noreply.github.com>
Date: Tue, 4 Feb 2025 21:13:24 +0100
Subject: [PATCH] illustration of Prop (#125)

---
 .../inductive-witnesses/TransitiveClosure.scala     | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/tutorials/inductive-witnesses/TransitiveClosure.scala b/tutorials/inductive-witnesses/TransitiveClosure.scala
index a9e610f0..b3804014 100644
--- 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