Tesla Zhang‮

ping

> Type checking for `match` is implemented by reusing the `elabClausesClassified`. > However, currently not even the simplest case would pass, due to some weird patterns being generated in the...

> I've looked into this issue yesterday, and one problem is that `ExprTraversal` does not visit patterns. > This makes the pattern preprocessing logic applies to function declaration with pattern...

@wsx-ucb from now on, you no longer need to regenerate the lexer. Only the parser. Yay!

We should have a meeting and discuss these changes.

> Like some RainbowVisitor? Well I'm not sure wdym by rainbow visitor. I think the one in intellij is unrelated

@imkiva I see. Seems I don't understand jb as much as you do lol

> We already have it: [SyntaxHighlight.java](https://github.com/aya-prover/aya-dev/blob/279ca6f63dd87da81f1873a9066f6f59bd3217f9/lsp/src/main/java/org/aya/lsp/actions/SyntaxHighlight.java). But it needs some generalization. Most likely we're going to migrate to GK so it should worth doing this task later

> > > We already have it: [SyntaxHighlight.java](https://github.com/aya-prover/aya-dev/blob/279ca6f63dd87da81f1873a9066f6f59bd3217f9/lsp/src/main/java/org/aya/lsp/actions/SyntaxHighlight.java). But it needs some generalization. > > > > Most likely we're going to migrate to GK so it should worth doing...

Now we can work on this!!