equal
deleted
inserted
replaced
447 fn genuine_only => fn [card, size] => |
447 fn genuine_only => fn [card, size] => |
448 (rpair NONE (iterate genuine_only (card, size) iterations)) |
448 (rpair NONE (iterate genuine_only (card, size) iterations)) |
449 end |
449 end |
450 end; |
450 end; |
451 |
451 |
452 fun size_matters_for _ Ts = not (forall |
452 val size_types = [@{type_name Enum.finite_1}, @{type_name Enum.finite_2}, |
453 (fn Type (tyco, []) => is_some (try (unprefix "Enum.finite") tyco) | _ => false) Ts) |
453 @{type_name Enum.finite_3}, @{type_name Enum.finite_4}, @{type_name Enum.finite_5}]; |
454 (*FIXME eliminate dynamic name reference*) |
454 |
|
455 fun size_matters_for _ Ts = |
|
456 not (forall (fn Type (tyco, []) => member (op =) size_types tyco | _ => false) Ts); |
455 |
457 |
456 val test_goals = |
458 val test_goals = |
457 Quickcheck_Common.generator_test_goal_terms ("random", (size_matters_for, compile_generator_expr)); |
459 Quickcheck_Common.generator_test_goal_terms ("random", (size_matters_for, compile_generator_expr)); |
458 |
460 |
459 (** setup **) |
461 (** setup **) |