equation compiler documentation

Stream: general

[Chris B]

Is there any documentation/reading material that details how the equation compiler does its thing?

[Sebastian Ullrich]

Let's just say there's a good reason we want to replace it

[Chris B]

Oh word. Is the desire to redo/simplify it or replace it with something else entirely? I like some of the user-facing ideas it presents quite a bit, but it can feel black box-ish at times (hence the docs question).

[Sebastian Ullrich]

I believe the plan is to both simplify it and make it customizable. Then users can implement the complicated rules themselves if they really need them, haha

[Chris B]

That would be really interesting. Does that also mean it could potentially be implemented in Lean?

[Sebastian Ullrich]

It definitely will be