Library HoTT.Basics.Logic
Set Implicit Arguments
.
Require
Export
Basics.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
.
#[
export
]
Hint
Unfold
not
:
core
.
#[
export
]
Hint
Resolve
I
:
core
.