author | haftmann |
Thu, 08 Nov 2018 09:11:52 +0100 | |
changeset 69260 | 0a9688695a1b |
parent 63731 | 9f906a2eb0e7 |
permissions | -rw-r--r-- |
63731
9f906a2eb0e7
added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff
changeset
|
1 |
theory Quickcheck_Nesting_Example |
9f906a2eb0e7
added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff
changeset
|
2 |
imports Quickcheck_Nesting |
9f906a2eb0e7
added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff
changeset
|
3 |
begin |
9f906a2eb0e7
added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff
changeset
|
4 |
|
9f906a2eb0e7
added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff
changeset
|
5 |
datatype x = X "x list" |
9f906a2eb0e7
added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff
changeset
|
6 |
|
9f906a2eb0e7
added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff
changeset
|
7 |
lemma "X a = X b" |
9f906a2eb0e7
added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff
changeset
|
8 |
quickcheck[exhaustive, size = 4, expect = counterexample] |
9f906a2eb0e7
added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff
changeset
|
9 |
oops |
9f906a2eb0e7
added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff
changeset
|
10 |
|
9f906a2eb0e7
added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff
changeset
|
11 |
end |