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 hoist operation and one with the value is a let, maybe in the future it will be a fix.
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.
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
199