| author | wenzelm |
| Thu, 15 Feb 2018 12:11:00 +0100 | |
| changeset 67613 | ce654b0e6d69 |
| 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 |