search

PatrickMassot / leanblueprint

plasTeX plugin to build formalization blueprints.
Apache License 2.0
136 stars 23 forks source link

Disconnect dependence on Lean 3 #4

Open mpenciak opened 2 years ago

mpenciak commented 2 years ago

As per the discussion on Zulip I've opened an issue to bring attention to this issue.

A tentative implementation of leanblueprint not using anything specific to Lean 3 is given here: https://github.com/mpenciak/noleanblueprint.