3 ms·

What exactly do these object files look like?

• kmill 1y ago
  The "olean" files are a binary format that contain everything that was added to the Lean environment. Among other things, it includes all of the declarations and their Lean.Expr [1] expressions. People have written tools to dump the data for inspection [2], or to independently check that the expressions are type correct and the environment is well-formed (that is, check the correctness). [1] https://github.com/leanprover/lean4/blob/3a3c816a27c0bd454711e2f9e4e20cbbde47ba85/src/Lean/Expr.lean#L302 https://github.com/leanprover/lean4/blob/3a3c816a27c0bd45471... [2] https://github.com/digama0/oleandump https://github.com/digama0/oleandump [3] https://github.com/ammkrn/nanoda_lib https://github.com/ammkrn/nanoda_lib