syntax: drop grade and support hoist #209
Merged
Conversation
This file contains 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
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.
Goals
Prepare syntax for MVP features.
Context
One of the targets of the MVP is to support inductive types properly, those are going to be achieved through dependent intersections and fixpoints, currently there is no way of defining a fixpoint in the Teika syntax, this solves that by supporting
x : A; M, this is very similar to Agda.To achieve this the main change is related to allowing annotations without parens on the left side of bindings, a binding without a value is a
hoistoperation and one with the value is alet, maybe in the future it will be afix.Grading syntax was also dropped as it will not be initially supported.
Additionally I'm using a more standard wrapping, closer to how the typed tree is defined.
Related