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