refactor(Modal): bot/imp/box primitives for modal propositions#636
Closed
benbrastmckie wants to merge 1 commit into
Closed
refactor(Modal): bot/imp/box primitives for modal propositions#636benbrastmckie wants to merge 1 commit into
benbrastmckie wants to merge 1 commit into
Conversation
benbrastmckie
requested review from
arademaker,
chenson2018 and
fmontesi
as code owners
benbrastmckie
added a commit
to benbrastmckie/cslib
that referenced
this pull request
Jun 12, 2026
- Restore LogicalEquivalence typeclass instantiation (HasContext, IsEquiv, Congruence, HasHContext, LogicalEquivalence) following the HML pattern, adapted for Lukasiewicz primitives - Add Proposition.Equiv parametric on model class S with notation - Fix copyright: restore Fabrizio Montesi as co-author on LogicalEquivalence.lean - Fix "fork's" artifact in docstring - Fix "satifies" typo in Basic.lean - Simplify redundant have in t_box_diamond proof Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Refactors Modal/Basic.lean from {atom, not, and, diamond} primitives to
{atom, bot, imp, box}, following the Lukasiewicz convention. Derived
connectives (neg, and, or, top, diamond, iff) defined as abbrevs.
All grind-based proofs replaced with explicit term-mode proofs.
Denotation.lean and LogicalEquivalence.lean updated for new primitives.
LogicalEquivalence typeclass fully instantiated following HML pattern.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
benbrastmckie
force-pushed
the
refactor/modal-lukasiewicz
branch
from
de5dc80 to
9337dd9
Compare
Author
|
Superseded by new PR with corrected branch name and terminology (removed inaccurate Lukasiewicz attribution). |
benbrastmckie
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Superseded by #637 (branch rename and terminology corrections).