Take generated constants into account #162

Closed
opened 2025-01-18 12:16:49 -08:00 by aniva · 2 comments
Owner

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

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
part/Delation
priority
medium
part/Goal
category
bug
labels 2025-01-18 12:16:49 -08:00
aniva self-assigned this 2025-01-18 12:16:49 -08:00
Author
Owner

Need an example ...

Need an example ...
aniva closed this issue 2025-01-24 15:06:34 -08:00
aniva reopened this issue 2025-01-24 15:06:36 -08:00
aniva added a new dependency 2025-01-31 13:16:37 -08:00
Author
Owner

Done #166

Done #166
aniva closed this issue 2025-01-31 13:16:42 -08:00
Sign in to join this conversation.
No Milestone
No project
No Assignees
1 Participants
Notifications
Due Date
The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Reference: aniva/Pantograph#162
No description provided.