Skip to content

notP is defined twice #1774

@affeldt-aist

Description

@affeldt-aist

in contra.v:

Definition notP {nP P} := MoveView (@lax_notP false nP P).

and in boolp.v:

Lemma notP (P : Prop) : ~ ~ P <-> P.

causing different behaviors according to which module is require imported.

Metadata

Metadata

Assignees

No one assigned

    Labels

    "bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions