Update format & lean, handle mdata

[ammkrn]

nanoda_lib assumes these changes; if you're ready to pull the trigger, here's the PR. If you want to keep it in a separate branch for now, I'm fine with that too, I'll update the checker's readme.

@siddhartha-gadgil this will be a small but breaking change relative to what you were doing. Please jump in if you have any concerns.

[siddhartha-gadgil]

What does it break @ammkrn ?

I was working on porting trepplein though that is on hold for a while. I can adapt as long as the export format is as documented and has enough information for a typechecker.

[siddhartha-gadgil]

Perhaps this breaks some hacks I had about spaces at the end of lines. If so that is fine - I will implement a better solution than the hacks.

[ammkrn]

The breaks should only require adjustments in the parser, the logical components of your checker should be unaffected. The parser breaks should be that theorem and opaque now have their own tags instead of using #DEF, definition lines have the reduction hint included, quotient is now four separate declarations instead of one #QUOT tag, and the contents of inductive/constructor lines have changed slightly.

The updated format is laid out in full in the updated README.

mdata nodes are pruned, but that shouldn't be breaking since the underlying expressions are still exported.