Take generated constants into account #162

New Issue

aniva · 2025-01-18T12:16:49-08:00

aniva commented

2025-01-18 12:16:49 -08:00

In the draft tactic, generation of additional constants may create unsoundness. Vide

Detect generation of new constants

In the draft tactic, generation of additional constants may create unsoundness. Vide - [Detect generation of new constants](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Detect.20generation.20of.20new.20constants.20in.20elaboration/near/494550641)

aniva added this to the 0.3 milestone 2025-01-18 12:16:49 -08:00

aniva added the

labels 2025-01-18 12:16:49 -08:00

aniva self-assigned this 2025-01-18 12:16:49 -08:00

Sign in to join this conversation.