From b5a2fa0d8321137b3f25ddac99527b3bef2e5f3a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 24 Oct 2024 11:34:09 +0200
Subject: [PATCH] doc: update README

---
 README.md | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/README.md b/README.md
index 7665af4..6673208 100644
--- a/README.md
+++ b/README.md
@@ -7,6 +7,16 @@ If you are using built in types Plausible is usually able to handle them already
 import Plausible
 
 example (xs ys : Array Nat) : xs.size = ys.size → xs = ys := by
+  /--
+  ===================
+  Found a counter-example!
+  xs := #[0]
+  ys := #[1]
+  guard: 1 = 1
+  issue: #[0] = #[1] does not hold
+  (0 shrinks)
+  -------------------
+  -/
   plausible
 
 #eval Plausible.Testable.check <| ∀ (xs ys : Array Nat), xs.size = ys.size → xs = ys
@@ -36,6 +46,7 @@ instance : SampleableExt MyType :=
     let xyDiff ← SampleableExt.interpSample Nat
     return ⟨x, x + xyDiff, by omega⟩
 
+-- No counter example found
 #eval Testable.check <| ∀ a b : MyType, a.y ≤ b.x → a.x ≤ b.y
 ```
 For more documentation refer to the module docs.