The aim is to create a bare-bones version of LeanInk that can be used to extract and log the data of tactics and goals from mathlib4. The changes pushed here are meant to steadily strip away details from the LeanInk source code until the bare-bones code is left.
0art0
commented
1 year ago
Description
The aim is to create a bare-bones version of
LeanInkthat can be used to extract and log the data of tactics and goals frommathlib4. The changes pushed here are meant to steadily strip away details from theLeanInksource code until the bare-bones code is left.Notable Changes
Additional Notes