Add toSortedAList defs to sptree compset

HOL-Theorem-Prover · Jan 12, 2024 · 3824244 · 3824244
1 parent b9c6ac5
commit 3824244
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/src/finite_maps/sptreeLib.sml b/src/finite_maps/sptreeLib.sml
@@ -66,6 +66,8 @@ fun add_sptree_compset compset =
       open sptreeTheory
     in
       computeLib.add_thms [
+        apsnd_cons_def,
+        combine_rle_def,
         delete_compute,
         difference_def,
         filter_v_def,
@@ -85,8 +87,12 @@ fun add_sptree_compset compset =
         mk_BS_def,
         mk_wf_def,
         size_def,
+        spt_center_def,
+        spt_centers_def,
+        spts_to_alist_def,
         toListA_def,
         toList_def,
+        toSortedAList_def,
         union_def,
         wf_def
       ] compset