Commits: 1a5bfcae by Jean-Alexandre Barszcz at 2020-07-28T22:51:58-04:00 Delay parsing of declarations until elaboration for define-operator
- elab.ml (lexp_p_decls): Add a parameter for unparsed tokens, so that
later declarations can be parsed in a context with newly declared operators
Looks good, thanks.
b5f1c7d5 by Jean-Alexandre Barszcz at 2020-07-28T22:51:58-04:00 Remove the parsing error for tightly binding postfix operators
Looks good, but in the comment, please mention that we used to signal an error and include an example that shows a case where signaling an error is a bad idea (e.g. the case against which you bumped).
ee058a31 by Jean-Alexandre Barszcz at 2020-07-28T22:51:59-04:00 Dump the evaluation context when the variable names don't match
Fair enough.
5295751f by Jean-Alexandre Barszcz at 2020-07-28T22:51:59-04:00 Assign the builtins Int.+, etc to suitable variables Int_+, etc.
_+_ can be Int.+ by default, but we should also keep that value in Int_+ in case _+_ gets reassigned (with a num typeclass, for instance).
Fine. As you may have noticed, the intention is to have `Int` be overloaded to mean both "the type `Int`" and "a module/tuple with fields `+`, `-`, ...".
I'm not yet sure how to do the overloading, but I was thinking of adding some support for coercions, so a module M could be coerced to M.t when a type is expected (similarly a type level `ℓ` could be coerced to `Type ℓ` when a type is expected).
Those 4 commits can go to `master`.
Stefan