equal
deleted
inserted
replaced
28 |
28 |
29 fun mk_if cond = Const (@{const_name Predicate.if_pred}, |
29 fun mk_if cond = Const (@{const_name Predicate.if_pred}, |
30 HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond; |
30 HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond; |
31 |
31 |
32 fun mk_iterate_upto T (f, from, to) = |
32 fun mk_iterate_upto T (f, from, to) = |
33 list_comb (Const (@{const_name Code_Numeral.iterate_upto}, |
33 list_comb (Const (@{const_name Predicate.iterate_upto}, |
34 [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_monadT T), |
34 [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_monadT T), |
35 [f, from, to]) |
35 [f, from, to]) |
36 |
36 |
37 fun mk_not t = |
37 fun mk_not t = |
38 let |
38 let |