chore(library/logic): fix comments
This commit is contained in:
parent
73aa024c31
commit
e91a64fb38
3 changed files with 3 additions and 3 deletions
|
@ -3,7 +3,7 @@
|
||||||
-- Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
|
-- Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
|
||||||
import .prop
|
import .prop
|
||||||
|
|
||||||
-- logic.connectives.eq
|
-- logic.eq
|
||||||
-- ====================
|
-- ====================
|
||||||
|
|
||||||
-- Equality.
|
-- Equality.
|
||||||
|
|
|
@ -6,7 +6,7 @@
|
||||||
-- ============================
|
-- ============================
|
||||||
|
|
||||||
-- Useful logical identities. In the absence of propositional extensionality, some of the
|
-- Useful logical identities. In the absence of propositional extensionality, some of the
|
||||||
-- calculations use the type class support provided by logic.connectives.instances
|
-- calculations use the type class support provided by logic.instances
|
||||||
|
|
||||||
import logic.instances logic.decidable logic.quantifiers logic.cast
|
import logic.instances logic.decidable logic.quantifiers logic.cast
|
||||||
|
|
||||||
|
|
|
@ -2,7 +2,7 @@
|
||||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
-- Author: Jeremy Avigad
|
-- Author: Jeremy Avigad
|
||||||
|
|
||||||
-- logic.core.instances
|
-- logic.instances
|
||||||
-- ====================
|
-- ====================
|
||||||
|
|
||||||
import logic.connectives algebra.relation
|
import logic.connectives algebra.relation
|
||||||
|
|
Loading…
Add table
Reference in a new issue