Skip to content

Misc improvements to `head` and `tail` functions for lists

Robbert Krebbers requested to merge robbert/head_tail into master
  • Define head as notation that prints (Coq defines it as parsing only).
  • Declare tail as simpl nomatch.
  • Add lemmas about head and tail.
Edited by Robbert Krebbers

Merge request reports