Skip to content
Permalink
Browse files

Fix name changes due to previous commit

Closes #683
  • Loading branch information...
myreen committed Sep 7, 2019
1 parent 0fa2cdf commit 26f4bae8dd00abd7a5ed6212dd12cda0d3d99af5
Showing with 7 additions and 7 deletions.
  1. +2 −2 basis/StringProgScript.sml
  2. +5 −5 basis/VectorProgScript.sml
@@ -174,7 +174,7 @@ val _ = translate mlstring_gt_def;

val _ = ml_prog_update open_local_block;
val result = translate collate_aux_def;
val collate_aux_side_def = theorem"collate_aux_1_side_def";
val collate_aux_side_def = theorem"collate_aux_side_def";
val _ = ml_prog_update open_local_in_block;

val _ = next_ml_names := ["collate"];
@@ -185,7 +185,7 @@ val collate_aux_side_thm = Q.prove (
`!f s1 s2 ord n len. (n + len =
if strlen s1 < strlen s2
then strlen s1
else strlen s2) ==> collate_aux_1_side f s1 s2 ord n len`,
else strlen s2) ==> collate_aux_side f s1 s2 ord n len`,
Induct_on `len` \\ rw [Once collate_aux_side_def]);

val collate_side_thm = Q.prove (
@@ -51,20 +51,20 @@ val result = translate mapi_def;

val _ = ml_prog_update open_local_block;
val result = translate foldli_aux_def;
val foldli_aux_1_side_def = theorem"foldli_aux_1_side_def"
val foldli_aux_side_def = theorem"foldli_aux_side_def"
val _ = ml_prog_update open_local_in_block;

val _ = next_ml_names := ["foldli"];
val result = translate foldli_def;
val foldli_side_def = definition"foldli_side_def";

val foldli_aux_1_side_thm = Q.prove(
`!f e vec n len. n + len = length vec ==> foldli_aux_1_side f e vec n len`,
Induct_on`len` \\ rw[Once foldli_aux_1_side_def]);
val foldli_aux_side_thm = Q.prove(
`!f e vec n len. n + len = length vec ==> foldli_aux_side f e vec n len`,
Induct_on`len` \\ rw[Once foldli_aux_side_def]);

val foldli_side_thm = Q.prove(
`foldli_side f e vec`,
rw[foldli_side_def,foldli_aux_1_side_thm]) |> update_precondition;
rw[foldli_side_def,foldli_aux_side_thm]) |> update_precondition;

val _ = ml_prog_update open_local_block;
val result = translate foldl_aux_def;

0 comments on commit 26f4bae

Please sign in to comment.
You can’t perform that action at this time.