(*  Title:      nominal_library.ML
    Author:     Christian Urban

  Basic function for nominal.
*)

signature NOMINAL_LIBRARY =
sig
  val mk_minus: term -> term
  val mk_perm: term -> term -> term
end


structure Nominal_Library: NOMINAL_LIBRARY =
struct

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

fun mk_perm p trm =
let
  val ty = fastype_of trm
in
  Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm
end



end (* structure *)

open Nominal_Library;