search

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4
Apache License 2.0
43 stars 15 forks source link

feat: parse tspps from ast export #136

Closed dselsam closed 2 years ago

dselsam commented 2 years ago

sister PR to https://github.com/leanprover-community/lean/pull/702 not designed to be merged until that PR propagates

cc: @PatrickMassot

dselsam commented 2 years ago

Replaced by https://github.com/leanprover-community/mathport/pull/138