Skip to content

Commit 066bfa6

Browse files
authored
refactor: Remove Neighborhood Semantics for Modal Logic (#818)
1 parent 4a7dd13 commit 066bfa6

42 files changed

Lines changed: 0 additions & 4851 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

Foundation.lean

Lines changed: 0 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -367,47 +367,6 @@ public import Foundation.Modal.ModalCompanion.Standard.KC
367367
public import Foundation.Modal.ModalCompanion.Standard.LC
368368
public import Foundation.Modal.Modality.Basic
369369
public import Foundation.Modal.Modality.S5
370-
public import Foundation.Modal.Neighborhood.AxiomC
371-
public import Foundation.Modal.Neighborhood.AxiomGeach
372-
public import Foundation.Modal.Neighborhood.AxiomK
373-
public import Foundation.Modal.Neighborhood.AxiomM
374-
public import Foundation.Modal.Neighborhood.AxiomN
375-
public import Foundation.Modal.Neighborhood.AxiomP
376-
public import Foundation.Modal.Neighborhood.Basic
377-
public import Foundation.Modal.Neighborhood.Completeness
378-
public import Foundation.Modal.Neighborhood.Filtration
379-
public import Foundation.Modal.Neighborhood.Hilbert
380-
public import Foundation.Modal.Neighborhood.IntersectionClosure
381-
public import Foundation.Modal.Neighborhood.Logic.E
382-
public import Foundation.Modal.Neighborhood.Logic.E4
383-
public import Foundation.Modal.Neighborhood.Logic.E5
384-
public import Foundation.Modal.Neighborhood.Logic.EB
385-
public import Foundation.Modal.Neighborhood.Logic.EC
386-
public import Foundation.Modal.Neighborhood.Logic.ECN
387-
public import Foundation.Modal.Neighborhood.Logic.ED
388-
public import Foundation.Modal.Neighborhood.Logic.EK
389-
public import Foundation.Modal.Neighborhood.Logic.EM
390-
public import Foundation.Modal.Neighborhood.Logic.EMC
391-
public import Foundation.Modal.Neighborhood.Logic.EMC4
392-
public import Foundation.Modal.Neighborhood.Logic.EMCN
393-
public import Foundation.Modal.Neighborhood.Logic.EMCN4
394-
public import Foundation.Modal.Neighborhood.Logic.EMK
395-
public import Foundation.Modal.Neighborhood.Logic.EMN
396-
public import Foundation.Modal.Neighborhood.Logic.EMNT4
397-
public import Foundation.Modal.Neighborhood.Logic.EMT
398-
public import Foundation.Modal.Neighborhood.Logic.EMT4
399-
public import Foundation.Modal.Neighborhood.Logic.EN
400-
public import Foundation.Modal.Neighborhood.Logic.EN4
401-
public import Foundation.Modal.Neighborhood.Logic.END
402-
public import Foundation.Modal.Neighborhood.Logic.END4
403-
public import Foundation.Modal.Neighborhood.Logic.ENT4
404-
public import Foundation.Modal.Neighborhood.Logic.EP
405-
public import Foundation.Modal.Neighborhood.Logic.ET
406-
public import Foundation.Modal.Neighborhood.Logic.ET4
407-
public import Foundation.Modal.Neighborhood.Logic.ET5
408-
public import Foundation.Modal.Neighborhood.Logic.ETB
409-
public import Foundation.Modal.Neighborhood.Logic.Incomparability.ED_EP
410-
public import Foundation.Modal.Neighborhood.Supplementation
411370
public import Foundation.Modal.PLoN.Basic
412371
public import Foundation.Modal.PLoN.Completeness
413372
public import Foundation.Modal.PLoN.Hilbert

Foundation/Modal/Neighborhood/AxiomC.lean

Lines changed: 0 additions & 82 deletions
This file was deleted.

0 commit comments

Comments
 (0)