Skip to content

Redundant top in modal formula definition #824

Open
Open
Redundant top in modal formula definition#824

Description

@SnO2WMaN
SnO2WMaN
opened on Jun 18, 2026

Foundation/Foundation/Modal/Formula/Basic.lean

Line 31 in c28942b

abbrev top : Formula α := imp falsum falsum

なぜか verum と top を２つ定義していた．

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions