aniva/Pantograph

Add unsafe detection in goal.print #151

New issue

Closed

opened 2024-12-19 05:02:52 -08:00 by aniva · 2 comments

aniva commented

2024-12-19 05:02:52 -08:00

Owner

This is to address an older concern about having unsafe.

Detection is optional.

This is to address an older concern about having unsafe. Detection is optional.

aniva added the

labels

2024-12-19 05:02:52 -08:00

aniva self-assigned this

2024-12-19 05:02:52 -08:00

aniva added this to the v0.3.1 milestone

2025-04-10 23:20:49 -07:00

aniva commented

2025-04-25 08:21:40 -07:00

Author

Owner

We should also output messages after a tactic to service things such as trace_state.

After each tactic, we can report whether the proof expression created in the mvars and delayed mvars have sorrys

We should also output messages after a tactic to service things such as `trace_state`. After each tactic, we can report whether the proof expression created in the mvars and delayed mvars have `sorry`s

aniva added a new dependency

2025-05-01 10:41:31 -07:00

#201 feat(goal): Detect unsafe and sorry

aniva commented

2025-05-01 10:41:34 -07:00

Author

Owner

#201

aniva closed this issue

2025-05-01 10:41:34 -07: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

#201 feat(goal): Detect unsafe and sorry

aniva/Pantograph

Reference: aniva/Pantograph#151

No description provided.