aniva/Pantograph

Take generated constants into account #162

New issue

Closed

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

aniva commented

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

Owner

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 v0.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

aniva commented

2025-01-24 15:06:34 -08:00

Author

Owner

Need an example ...

Need an example ...

aniva added a new dependency

2025-01-31 13:16:37 -08:00

#166 fix: Use in-context environment in sorry collection

aniva commented

2025-01-31 13:16:42 -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 labels

part/Environment

pending-measurement

No milestone

No project

No assignees

1 participant

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Depends on

#166 fix: Use in-context environment in sorry collection

aniva/Pantograph

Reference: aniva/Pantograph#162

No description provided.