equal
deleted
inserted
replaced
1 theory RPred |
1 theory RPred |
2 imports Quickcheck Random Predicate |
2 imports Quickcheck Random Predicate |
3 begin |
3 begin |
4 |
4 |
5 types 'a "rpred" = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)" |
5 type_synonym 'a "rpred" = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)" |
6 |
6 |
7 section {* The RandomPred Monad *} |
7 section {* The RandomPred Monad *} |
8 |
8 |
9 text {* A monad to combine the random state monad and the predicate monad *} |
9 text {* A monad to combine the random state monad and the predicate monad *} |
10 |
10 |