1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
From QuickChick Require Import QuickChick.
(* TODO: better naming *)
Inductive foo {A : Type} :=
| bar : A -> foo -> foo
| baz : foo
.
Derive (Arbitrary, Show) for foo.
Sample (arbitrary : G foo).
Section Sanity.
Inductive qux : Type :=
| Qux: forall {A: Type}, A -> qux.
Definition quux: qux -> bool :=
fun a => match a with | Qux a => true end.
End Sanity.
Section Failures.
Set Asymmetric Patterns.
Fail Definition quux': qux -> bool :=
fun a => match a with | Qux a => true end.
End Failures.
Import MonadNotation.
Definition a : G nat :=
ret 1.
Definition b : G nat :=
v <- a ;;
ret v.
Import BindOptNotation.
Definition c : G (option nat) :=
ret (Some 42).
Definition d : G (option nat) :=
v <-- c;;
ret (Some v).
Sample a.
Sample b.
Sample (liftM Some a).
Sample c.
Sample d.
Set Warnings "-notation-overridden".
From mathcomp Require Import ssreflect ssrnat div.
QuickChick
(fun (s : nat) (t : nat) =>
eqn
(gcdn s t)
(gcdn t s)).
(* Test extraction hack (substitute type int = int) *)
Definition int := nat.
Definition teh := fun x : int => Nat.eqb x x.
QuickChick teh.
|
