Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use explicit persistence again #421

Merged
merged 3 commits into from May 7, 2023
Merged

Use explicit persistence again #421

merged 3 commits into from May 7, 2023

Conversation

Blaisorblade
Copy link
Owner

@Blaisorblade Blaisorblade commented Aug 27, 2022

Instead of proving (once and for all) that all our propositions are persistent, use the persistence modality explicitly. See #428 for motivation.

TODO:

  • add instances for Persistent and IntoPersistent for all judgments in the right places
  • for path equivalences, add/start using types of persistent relations (maybe by building on iPPred in lty.v, despite the asymmetry).

Base automatically changed from tweaks to master August 27, 2022 01:51
@Blaisorblade Blaisorblade force-pushed the persistence-back branch 8 times, most recently from 9112992 to 18d94a0 Compare August 29, 2022 11:58
@Blaisorblade Blaisorblade force-pushed the persistence-back branch 2 times, most recently from b3850a4 to 6a37432 Compare August 29, 2022 12:18
@Blaisorblade Blaisorblade self-assigned this Sep 4, 2022
@Blaisorblade Blaisorblade changed the base branch from master to pupd-prepare-2 September 5, 2022 00:24
Base automatically changed from pupd-prepare-2 to master September 5, 2022 00:27
@Blaisorblade Blaisorblade force-pushed the persistence-back branch 2 times, most recently from e3773fa to f5863d5 Compare April 16, 2023 01:00
@Blaisorblade Blaisorblade marked this pull request as ready for review May 7, 2023 14:06
@Blaisorblade Blaisorblade merged commit a3c2f09 into master May 7, 2023
2 checks passed
@Blaisorblade Blaisorblade deleted the persistence-back branch May 7, 2023 14:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

1 participant