From 5d4b6a3de22d239dac01a46963672851a027b952 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 30 Nov 2014 21:19:56 -0800 Subject: [PATCH] chore(library/logic/logic.md): adjust documentation --- library/logic/logic.md | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) diff --git a/library/logic/logic.md b/library/logic/logic.md index 8397c18fd..c86ef3c66 100644 --- a/library/logic/logic.md +++ b/library/logic/logic.md @@ -1,26 +1,16 @@ logic ===== -Logical constructions and axioms. By default, `import logic` does not -import any additional axioms. +Additional constructions and axioms. By default, `import logic` does not +import any axioms. Logical operations and connectives. -* [prop](prop.lean) : the type Prop -* [eq](eq.lean) : equality and disequality -* [connectives](connectives.lean) : propositional connectives +* [eq](eq.lean) : additional theorems for equality and disequality * [cast](cast.lean) : casts and heterogeneous equality * [quantifiers](quantifiers.lean) : existential and universal quantifiers -* [if](if.lean) : if-then-else * [identities](identities.lean) : some useful identities -Type classes for general logical manipulations: - -* [inhabited](inhabited.lean) : inhabited types -* [nonempty](nonempty.lean) : nonempty type -* [decidable](decidable.lean) : decidable types -* [instances](instances.lean) : type class instances - Constructively, inhabited types have a witness, while nonempty types are "proof irrelevant". Classically (assuming the axioms in logic.axioms.hilbert) the two are equivalent. Type class inferences