parsingcheck-410.v « coq « etc - proof-general - Emacs interface for proof assistants

about summary refs log tree commit diff homepage

path: root/etc/coq/parsingcheck-410.v

blob: 37a7e57fcdf15e5a25e2a9635191e5cd76549e49 (plain)

1
2
3

Require Export Coq.Lists.List. 
Notation "[ ]" := nil : list_scope. 
Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.