Position Info Support - Githubissues

dselsam / binport

A tool for building Lean4 .olean files from Lean3 export data

Apache License 2.0

10 stars 1 forks source link

Position Info Support #26

Open AurelienSaue opened 3 years ago

AurelienSaue commented 3 years ago

I have added support for #POS_INFO by adding the corresponding DeclarationRanges (with all fields filled with the only position given by the #POS_INFO).

I believe this can be useful if we want to create source files:

to print the declarations in the right order
and to delete auto-generated declarations like ._proof_1, by using the fact that they all share the same position info.

dselsam commented 3 years ago

@AurelienSaue Thanks! I'll merge this next time I run the pipeline.