Now, the following example produces a syntax error.
```lean
macro "foo!" x:term : term => `($x + 1)
check id foo! 10
```
@Kha, I think the heuristic is simple and defensible.
If the new syntax starts and ends with token, than the precedence is
`maxPrec`. Otherwise, it is `leadPrec`.
see #180
@Kha Before this commit, we were producing the error "expected command" at the `let` token
```lean
check id let x := 1; x
```
The new error is "expected command, but found term; this error may be
due to parsing precedence levels, consider parenthesizing the term".
The example above looks artificial, but it will happen all the time as
users start to define their own notation.
@Kha I suspect the memory leaks reported at the CI are due to
an exception produced by the compiler.
The compiler is currently a mix of Lean and C++ code.
I think the exception was thrown from C++ code, crossed Lean code (producing
memory leaks), and was caught by the old frontend written in C++.
We will eventually replace the compiler C++ code with Lean code.
So, I think this is a low priority issue.
The motivation is to prevent users from tinkering with its internal
implementation details that rely on unsafe features.
The new test crashed before this commit.
@Kha I wrote this extended test using the new frontend. The new
frontend worked great. I only had a minor issue with `#exit`.
The example uses `let rec`, parsers, macros, lift-method notation, etc.
It implements the new parser `strInterpolant p` for string
interpolation. The parser `p` is used to process the elements inside
`{...}`. Then, I use this parser to implement the macro `toString!`.
Example: `toString! "1+2 = {1+2}"` produces `"1+2 = 3"`.
Even the new "lift-method" notation works inside the string interpolant.
```lean
def g (x : Nat) : StateRefT Nat IO Nat := do
modify (· + x);
get
def ex : StateRefT Nat IO Unit := do
IO.println $ toString! ">> hello {(<- g 1)}";
IO.println $ toString! ">> world {(<- g 1)}";
pure ()
```
@Kha `hygienicIntro` is true by default. `hygienicIntro == false` is
the Lean3 behavior. If we find `hygienicIntro` too inconvenient in
practice, we set the default to false.
It preserves the location of the local declaration.
@Kha This tactic is going to be used to fix another hygiene related bug in
Lean3 :)
Here is small repro for the problem.
```
example (m n k : ℕ) (h : 0 + n = m) (h : k = m) : ... :=
begin
-- Here `h : k = m` is accessible.
rw [nat.zero_add] at *
-- `h : k = m` is not accessible anymore, and it is a name for
-- the simplified `h : n = m` which was inaccessible before.
end
```
@Kha Not sure whether we should have an option for supressing this
information or not.
We need this information for diagnosing problems. For example, I was trying to
understand why the elaborator was looping. I suspected it was the
TC module, but I was not getting any trace messages since the symbol
was overloaded, and the case that did not work was the expensive one :(
