equal
deleted
inserted
replaced
537 [code_unfold]: "pmfify A x = |
537 [code_unfold]: "pmfify A x = |
538 Code_Evaluation.valtermify pmf_of_multiset {\<cdot>} |
538 Code_Evaluation.valtermify pmf_of_multiset {\<cdot>} |
539 (Code_Evaluation.valtermify (+) {\<cdot>} A {\<cdot>} |
539 (Code_Evaluation.valtermify (+) {\<cdot>} A {\<cdot>} |
540 (Code_Evaluation.valtermify single {\<cdot>} x))" |
540 (Code_Evaluation.valtermify single {\<cdot>} x))" |
541 |
541 |
542 |
|
543 notation fcomp (infixl "\<circ>>" 60) |
|
544 notation scomp (infixl "\<circ>\<rightarrow>" 60) |
|
545 |
|
546 instantiation pmf :: (random) random |
542 instantiation pmf :: (random) random |
|
543 begin |
|
544 |
|
545 context |
|
546 includes state_combinator_syntax |
547 begin |
547 begin |
548 |
548 |
549 definition |
549 definition |
550 "Quickcheck_Random.random i = |
550 "Quickcheck_Random.random i = |
551 Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>A. |
551 Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>A. |
553 |
553 |
554 instance .. |
554 instance .. |
555 |
555 |
556 end |
556 end |
557 |
557 |
558 no_notation fcomp (infixl "\<circ>>" 60) |
558 end |
559 no_notation scomp (infixl "\<circ>\<rightarrow>" 60) |
|
560 |
559 |
561 instantiation pmf :: (full_exhaustive) full_exhaustive |
560 instantiation pmf :: (full_exhaustive) full_exhaustive |
562 begin |
561 begin |
563 |
562 |
564 definition full_exhaustive_pmf :: "('a pmf \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" |
563 definition full_exhaustive_pmf :: "('a pmf \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" |