# 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.
Require List.
Export List.ListNotations.
Require Import Bvector.
Treating n-ary exists
Tactic Notation "exists" constr(x) := exists x.
Tactic Notation "exists" constr(x) constr(y) := exists x ; exists y.
Tactic Notation "exists" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z.
Tactic Notation "exists" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w.