termination for v_to_char_list_def

CakeML · Oct 14, 2014 · dc19e94 · dc19e94
1 parent 2763e05
commit dc19e94
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/semantics/terminationScript.sml b/semantics/terminationScript.sml
@@ -190,6 +190,11 @@ val (v_to_list_def,v_to_list_ind) =
 wf_rel_tac `measure v_size`);
 val _ = register "v_to_list" v_to_list_def v_to_list_ind;
 
+val (v_to_char_list_def,v_to_char_list_ind) =
+  tprove_no_defn ((v_to_char_list_def,v_to_char_list_ind),
+wf_rel_tac `measure v_size`);
+val _ = register "v_to_char_list" v_to_char_list_def v_to_char_list_ind;
+
 val check_ctor_foldr_flat_map = Q.prove (
 `!c. (FOLDR
          (λ(tvs,tn,condefs) x2.