1 (*  Title:      nominal_library.ML

     2     Author:     Christian Urban

     3 

     4   Basic function for nominal.

     5 *)

     6 

     7 signature NOMINAL_LIBRARY =

     8 sig

     9   val mk_minus: term -> term

    10   val mk_perm: term -> term -> term

    11 end

    12 

    13 

    14 structure Nominal_Library: NOMINAL_LIBRARY =

    15 struct

    16 

    17 fun mk_minus p = 

    18  Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p

    19 

    20 fun mk_perm p trm =

    21 let

    22   val ty = fastype_of trm

    23 in

    24   Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm

    25 end

    26 

    27 

    28 

    29 end (* structure *)

    30 

    31 open Nominal_Library;