4 

     5 (* test for get_fun *)

     6 datatype t =

     7    vr "string"

     8  | ap "t list"

     9  | lm "string" "t"

    10 

    11 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"

    12 axioms t_eq: "EQUIV Rt"

    13 

    14 quotient qt = "t" / "Rt"

    15     by (rule t_eq)

    16 

    17 setup {*

    18   maps_update @{type_name "list"} {mapfun = @{const_name "map"},      relfun = @{const_name "LIST_REL"}} #>

    19   maps_update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #>

    20   maps_update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}

    21 *}

    22 

    23 

    24 ML {*

    25 get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}

    26  |> fst

    27  |> Syntax.string_of_term @{context}

    28  |> writeln

    29 *}

    30 

    31 ML {*

    32 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"}

    33  |> fst

    34  |> Syntax.string_of_term @{context}

    35  |> writeln

    36 *}

    37 

    38 ML {*

    39 get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}

    40  |> fst

    41  |> Syntax.pretty_term @{context}

    42  |> Pretty.string_of

    43  |> writeln

    44 *}

    45 (* end test get_fun *)

    46