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

experimental fitch-style modal calculus #177

Merged
merged 62 commits into from
Jul 26, 2018
Merged

experimental fitch-style modal calculus #177

merged 62 commits into from
Jul 26, 2018

Conversation

jonsterling
Copy link
Collaborator

@jonsterling jonsterling commented Jul 24, 2018

Close #102, #178, #162

@jonsterling
Copy link
Collaborator Author

It looks like the behavior of the prev operator forces me to implement the typechecker in the other direction; rather than working my way up through the spine, I must work my way down. This is because there are context effects in the premises of the synthesis rules.

@jonsterling

This comment has been minimized.

@jonsterling
Copy link
Collaborator Author

Next step is to move to the version where dfix is a line constructor, between the fixed point and its unfolding.

Copy link
Collaborator

@favonia favonia left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See you later!

Copy link
Collaborator

@favonia favonia left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suspended approval forced.

classifier

let lookup_constant nm tw cx =
if cx.all_locks > 0 then
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This may not be necessary; i guess somehow every constant is a global element, and might as well have been defined inside the box modality.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, it's not quite as simple as that, but there is probably a story.

@jonsterling jonsterling merged commit 7f31814 into master Jul 26, 2018
@jonsterling jonsterling deleted the later-modality branch July 26, 2018 10:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants