Skip to content

Commit 2f0f3a9

Browse files
committed
Fix ListSplice.v
1 parent 8fe822d commit 2f0f3a9

File tree

2 files changed

+3
-1
lines changed

2 files changed

+3
-1
lines changed

src/Helpers/ListSplice.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,7 @@ Lemma list_splice_in_bounds l n l' :
8181
Proof.
8282
intros.
8383
rewrite /list_splice.
84-
rewrite Nat.min_l; [ lia | ].
84+
rewrite -> Nat.min_l by lia.
8585
rewrite (take_ge l') //.
8686
Qed.
8787

src/ShouldBuild.v

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,8 @@ From Perennial.goose_lang.lib Require
7474

7575
(* WIP Z-based list library *)
7676
From Perennial.Helpers Require ListZ.
77+
(* WIP list helper library *)
78+
From Perennial.Helpers Require ListSplice.
7779

7880
(* goose output *)
7981
From Goose.github_com.goose_lang.goose.internal.examples Require

0 commit comments

Comments
 (0)