Sequent.allQuest should return a Boolean. #72

Open

Labels

bot

opened

on Sep 24, 2025

cslib/Cslib/Logics/LinearLogic/CLL/Basic.lean

Lines 139 to 140 in 03c480f

    
           -- TODO: This should become a Bool. 
        
           /-- Checks that all propositions in `Γ` are question marks. -/

Metadata

Assignees

No one assigned

Labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests