Library Coq.Init.Logic

Set Implicit Arguments.

Require Export Notations.

Global Set Universe Polymorphism.
Global Set Asymmetric Patterns.

Notation "A -> B" := ( (_ : A), B) : type_scope.

Propositional connectives

True is the unit type.
Inductive True : Type :=
  I : True.

False is the empty type.
Inductive False : Type :=.

not A, written ¬A, is the negation of A
Definition not (A:Type) : Type := A False.

Hint Unfold not: core.

Hint Resolve I : core.