Matt: On Tue, Jul 1, 2014 at 10:12 AM, Matt Oliveri <[email protected]> wrote:
> The dependently-typed languages I'm most familiar with, Coq and Agda, > don't try to separate types and terms into sub-grammars... That's more or less what I thought. But it creates some interesting grammatical issues, notably at type-qualified expressions. If you have something like expr ':' type that can end up turning into expr : expr : type ... and so forth. And there *are* things in the type language that are not expressions. For example the names of the core types in the language. How does agda resolve this sort of thing? shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
