PatrickMassot / leanblueprint

plasTeX plugin to build formalization blueprints.
Apache License 2.0
158 stars 25 forks source link

Neutralize the mathlibok command #13

Closed Bergschaf closed 6 months ago

Bergschaf commented 6 months ago

I don't know to what extend the mathlibok command is supported in the new version, but I think it wouldn't hurt to neurtralize it in the print version, so it doesn't create any errors when running inv all. And I think the mathlibok command is nice, so I am planning to do some more PRs (for example color customization for the mathlibok nodes)

PatrickMassot commented 6 months ago

Thanks!