Pickle environment extensions #137

New Issue

aniva · 2024-12-08T16:11:48-08:00

aniva commented

2024-12-08 16:11:48 -08:00

Some tactics such as simp generates environment extensions. These should be pickled alongside the goal state or environment to ensure these tactics work properly.

https://leanprover.zulipchat.com/#narrow/channel/219941-Machine-Learning-for-Theorem-Proving/topic/Pantograph/near/486815694

Some tactics such as `simp` generates environment extensions. These should be pickled alongside the goal state or environment to ensure these tactics work properly. https://leanprover.zulipchat.com/#narrow/channel/219941-Machine-Learning-for-Theorem-Proving/topic/Pantograph/near/486815694

aniva added the

labels 2024-12-08 16:11:48 -08:00

aniva self-assigned this 2024-12-08 16:11:48 -08:00

aniva added this to the 0.2.22 milestone 2024-12-08 16:13:10 -08:00

aniva added the

priority

medium