1structure sortingSyntax :> sortingSyntax = 2struct 3 4open Abbrev HolKernel sortingTheory 5 6val binop = HolKernel.syntax_fns2 "sorting" 7val triop = HolKernel.syntax_fns3 "sorting" 8val quadop = HolKernel.syntax_fns4 "sorting" 9 10val (perm_tm, mk_perm, dest_perm, is_perm) = binop "PERM" 11val (sorted_tm, mk_sorted, dest_sorted, is_sorted) = binop "SORTED" 12val (qsort_tm, mk_qsort, dest_qsort, is_qsort) = binop "QSORT" 13val (qsort3_tm, mk_qsort3, dest_qsort3, is_qsort3) = binop "QSORT3" 14val (part_tm, mk_part, dest_part, is_part) = quadop "PART" 15val (part3_tm, mk_part3, dest_part3, is_part3) = triop "PART3" 16val (partition_tm, mk_partition, dest_partition, is_partition) = 17 binop "PARTITION" 18 19end 20