Leonardo de Moura
Leonardo de Moura
> How does the last option interact with caching? In last option, the system would not use any cache for coercions. We would rely on the fact that the number...
> If I see this correctly, we could register tactics to be run during type class resolution without disabling the cache, it just wouldn't help us with coercions. We'd just...
At #1674, we are considering a new elaborator which maps `syntax` to `expr`. It will be a good opportunity to implement this issue.
@gebner I'm trying to get back to Lean. I want to focus on other pending problems. It would be a big distraction for me a PR for this RFC.
> Are there any suggested workarounds? Use `@foo._match_1` full example: ```lean section parameter α : Type include α def foo : nat := match 0 with _ := 0 end...
> I believe that the best representation is whatever will be the syntax type from #1674. I agree.
> Aside from semantic highlighting, I don't see what this change would buy us. @gebner One issue is the goal visualization buffer. In the new approach, we would also store...
> There is also the highly hacky solution of having the server automatically preserving the most recently requested goal. This would require no editor cooperation and there is no chance...
> So it does look like we're mostly missing structured messages to implement the on-demand scheme. I was thinking of using serialized format objects for that before #1692 was opened,...
@kha I don't see any easy solution for this performance problem. It is very easy to get a huge number of cases. We can minimize the problem by generating custom...