Library Coq.Program.Syntax

Custom notations and implicits for Coq prelude definitions.
Author: Matthieu Sozeau Institution: LRI, CNRS UMR 8623 - University Paris Sud
Haskell-style notations for the unit type and value.

Notation " () " := Datatypes.unit : type_scope.
Notation " () " := tt.

Set maximally inserted implicit arguments for standard definitions.

Arguments Some {A} _.
Arguments None {A}.

Arguments pair {A B} _ _.
Arguments fst {A B} _.
Arguments snd {A B} _.

Arguments nil {A}.
Arguments cons {A} _ _.