Topic: olean files to source
Aurélien Saue (Apr 01 2021 at 10:35):
In an effort to convert the olean files created by
mathport into source files, I am trying to make a tool that is able to read olean files.
I have found the
readModuleData function from
Environment.lean which is able to read an olean file into a
toString on the contents gives a basic first result but could be improved a lot.
Do you know which better functions could be used to display the expressions?
Daniel Selsam (Apr 01 2021 at 15:03):
The delaborator (as in "de-elaborator") maps
Syntax, and can be customized e.g. by various
pp.<flag> options. It is here: https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Delaborator/Basic.lean#L382.
ppTerm goes from
Aurélien Saue (Apr 12 2021 at 09:58):
Using the delaborator as proposed I get fine results except that the implicit arguments of functions are displayed.
I guess I could solve that using the
pp.explicit option but I don't manage to pass the options because I don't understand how the
OptionsPerPos argument works or how to create it.
Could anyone help me a little?
Sebastian Ullrich (Apr 12 2021 at 10:00):
The implicit arguments are displayed? That should not be the default.
Aurélien Saue (Apr 12 2021 at 10:13):
Yes... Maybe the expressions I get with
readModuleData have nonly explicit arguments?
Aurélien Saue (Apr 12 2021 at 10:14):
I mean maybe the implicit arguments are stored as explicit in the
olean file so when I try to extract them back I cannot know if they were implicit or not
Aurélien Saue (Apr 12 2021 at 10:57):
What is weird is that in the function definitions all the implicit arguments are printed as implicit but in function applications the implicit arguments are displayed and there is no
@ before the function name
Last updated: May 07 2021 at 11:09 UTC