aboutsummaryrefslogtreecommitdiff
path: root/src/Util
diff options
context:
space:
mode:
authorGravatar jadep <jade.philipoom@gmail.com>2018-09-18 12:00:37 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2018-12-21 10:22:41 -0500
commit943d76f97fcbb02ca5d417266ad9dcd7a9561a73 (patch)
tree35113960fab7845b39314544f974220307cbcd33 /src/Util
parent9883e4e7a60ba7d1e1487f7a4501363bd3958fde (diff)
prove [eval_conditional_sub]
Diffstat (limited to 'src/Util')
-rw-r--r--src/Util/ListUtil.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 9f6658c42..cb11eca3b 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -1297,6 +1297,7 @@ Proof.
revert k a; induction b as [|? IHb], k; simpl; try reflexivity.
intros; rewrite IHb; reflexivity.
Qed.
+Hint Rewrite @firstn_seq : push_firstn.
Lemma skipn_seq k a b
: skipn k (seq a b) = seq (k + a) (b - k).