Hi, Am Dienstag, den 19.02.2019, 10:28 -0800 schrieb Iavor Diatchki:
I am a bit concerned with the notation though: in other places where we use `@a`, (e.g., #126 type application in patterns, and TypeApplications) the `a` is a type, while in this use it must be a variable. I wonder if this punning might be confusing. I don't really have an alternative suggestion though.
on the term level, lambda parameters are variables and function arguments are terms, without a different syntax here. So I think that is fine. Ok, there is a bit of syntactic sugar to allow patterns in lambdas. So maybe a future proposal can extend this to allow type patterns in lambdas… But I think I am fine doing small steps here. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/