Mario Carneiro

Is this actually a complete proof though? I'm not super familiar with the REPL API but I would expect some kind of qed-equivalent to complete the proof once all the...

> At present there is nothing you can do with a completed proof state: we would like to extend this so that you can replace the original sorry with your...

(I think you meant @digama0 )

The main thing that is implemented at this point is a full pipeline to check the MML. In particular that means it can start from the sources only and generate...

Yes, that's correct. (And I would ask why (1) should even be a goal; the main reason I can see it being useful is for the htmlizer, which makes use...

The section variable linter is not disableable, this issue is not actionable until that changes.

As I've mentioned in that thread and others, a major component to turning this into a tactic is delineating how precisely it should work. What information is tracked, what does...

Not good enough; you already want that statement for quotients, and isomorphisms are quotient maps. So there is another route to the theorem that you would want to have anyway.