fix: Tactics should produce `.syntheticOpaque` goals #100

Merged

aniva merged 2 commits from goal/tactic into dev

2024-10-03 08:47:31 -07:00

aniva commented

2024-09-08 14:14:26 -07:00

Owner

Didn't make it to 0.2.18, but this isn't very important. Lean's own tactics don't even produce .syntheticOpaque goals all the time, but this will be fixed in the future.

Didn't make it to 0.2.18, but this isn't very important. Lean's own tactics don't even produce `.syntheticOpaque` goals all the time, but this will be fixed in the future.

aniva added this to the 0.3 milestone 2024-09-08 14:14:26 -07:00

aniva added the

labels 2024-09-08 14:14:26 -07:00

aniva self-assigned this 2024-09-08 14:14:26 -07:00

aniva added 1 commit 2024-09-08 14:14:27 -07:00

5e99237e09

fix: Tactics should produce `.syntheticOpaque` goals

aniva added the

label 2024-09-08 14:25:04 -07:00

aniva commented

2024-09-09 17:24:57 -07:00

Author

Owner

Tracking https://github.com/leanprover/lean4/issues/5279

Tracking https://github.com/leanprover/lean4/issues/5279

aniva added 1 commit 2024-10-03 01:39:01 -07:00

ed1f96d7f7

Merge branch 'dev' into goal/tactic

aniva merged commit b174b4ea79 into dev

2024-10-03 08:47:31 -07:00

aniva referenced this issue from a commit

2024-10-03 08:47:32 -07:00

Merge pull request 'fix: Tactics should produce `.syntheticOpaque` goals' (#100) from goal/tactic into dev

aniva modified the milestone from 0.3 to 0.2.19

2024-10-05 22:41:29 -07:00

Sign in to join this conversation.

No reviewers

No Label

part/Environment

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#100

No description provided.