Add unsafe detection in goal.print #151

New Issue

aniva · 2024-12-19T05:02:52-08:00

aniva commented

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

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

part/Goal

category

feature

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 0.3.1 milestone 2025-04-10 23:20:49 -07:00

aniva commented

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

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

Sign in to join this conversation.

No Label

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.

Dependencies

No dependencies set.

Reference: aniva/Pantograph#151