diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-07 14:25:06 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-07 14:25:06 -0700 |
| commit | 7c2055d6039e4c7df2a40b6ca45f37416fc758a7 (patch) | |
| tree | d52b4ad21a2243c53c0975b6312912965c340dfa /src/Util/ListUtil.v | |
| parent | bd2fcf4e05bc6fd389be917fa52dcbfe08af5ec0 (diff) | |
Slightly better arguments in ListUtil
Diffstat (limited to 'src/Util/ListUtil.v')
| -rw-r--r-- | src/Util/ListUtil.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index fd592e3b9..62432b96c 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -322,13 +322,13 @@ Proof. destruct (nth_error_length_exists_value i xs); intuition; congruence. Qed. -Lemma nth_error_value_eq_nth_default : forall {T} i xs (x d:T), +Lemma nth_error_value_eq_nth_default : forall {T} i (x : T) xs, nth_error xs i = Some x -> forall d, nth_default d xs i = x. Proof. unfold nth_default; boring. Qed. -Hint Rewrite @nth_error_value_eq_nth_default using assumption : simpl_nth_default. +Hint Rewrite @nth_error_value_eq_nth_default using eassumption : simpl_nth_default. Lemma skipn0 : forall {T} (xs:list T), skipn 0 xs = xs. Proof. auto. Qed. |