Pickle proof object #203

New Issue

aniva · 2025-05-05T08:05:15-07:00

aniva commented

2025-05-05 08:05:15 -07:00

Given the buggy nature of Lean's delaborator, if we want to save a proof and check it later, we need a more robust object exchange format.

Pickling an expression along with its type does just that, but we need to also save any lemmas generated by the simplifier.

Given the buggy nature of Lean's delaborator, if we want to save a proof and check it later, we need a more robust object exchange format. Pickling an expression along with its type does just that, but we need to also save any lemmas generated by the simplifier.

aniva added this to the 0.3.2 milestone 2025-05-05 08:05:15 -07:00

aniva added the

category

feature

label 2025-05-05 08:05:15 -07:00

aniva self-assigned this 2025-05-05 08:05:15 -07:00

Sign in to join this conversation.