search

sorear / smetamath-rs

sorear's Metamath system engine - version 3 Rust
Apache License 2.0
22 stars 6 forks source link

Export mmp #32

Closed digama0 closed 8 years ago

digama0 commented 8 years ago

Adds support for producing mmp files compliant with mmj2.

sorear commented 8 years ago

Oh wow! I thought this was weeks away. I'll give it a look tomorrow.

sorear commented 8 years ago

LGTM once the perf regression is addressed, and I'm quite happy to handle that myself if you prefer

sorear commented 8 years ago

with your changes and my last change, performance is back to within measurement error of master, so this is in