Skip to content

Commit

Permalink
doc: update README
Browse files Browse the repository at this point in the history
  • Loading branch information
hargoniX committed Oct 24, 2024
1 parent 7ec34fe commit b5a2fa0
Showing 1 changed file with 11 additions and 0 deletions.
11 changes: 11 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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.

0 comments on commit b5a2fa0

Please sign in to comment.