src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
changeset 39466 f3c5da707f30
parent 39463 7ce0ed8dc4d6
child 39800 17e29ddd538e
equal deleted inserted replaced
39465:fcff6903595f 39466:f3c5da707f30
    16    limited_predicates = [],
    16    limited_predicates = [],
    17    replacing = [],
    17    replacing = [],
    18    manual_reorder = []}) *}
    18    manual_reorder = []}) *}
    19 
    19 
    20 values "{(x, y, z). append x y z}"
    20 values "{(x, y, z). append x y z}"
       
    21 
       
    22 values 4 "{(z, x, y). append x y ((1::nat) # (2 # (3 # z)))}"
    21 
    23 
    22 values 3 "{(x, y, z). append x y z}"
    24 values 3 "{(x, y, z). append x y z}"
    23 
    25 
    24 setup {* Code_Prolog.map_code_options (K
    26 setup {* Code_Prolog.map_code_options (K
    25   {ensure_groundness = false,
    27   {ensure_groundness = false,