Set Params and maximally implicits for `head` like other list functions.

09f69b7c · Robbert Krebbers · 1657d8d0 · 09f69b7c
Commit 09f69b7c authored May 03, 2019 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 0 deletions

theories/list.v theories/list.v +2 -0

No files found.
--- a/theories/list.v
+++ b/theories/list.v
@@ -18,10 +18,12 @@ Notation tail := tl.
 Notation take := firstn.
 Notation drop := skipn.

+Arguments head {_} _ : assert.
 Arguments tail {_} _ : assert.
 Arguments take {_} !_ !_ / : assert.
 Arguments drop {_} !_ !_ / : assert.

+Instance: Params (@head) 1 := {}.
 Instance: Params (@tail) 1 := {}.
 Instance: Params (@take) 1 := {}.
 Instance: Params (@drop) 1 := {}.