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
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
part/Goal
category
bug
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
aniva added the
priority
low
label 2024-09-08 14:25:04 -07:00
Author
Owner
Tracking https://github.com/leanprover/lean4/issues/5279
aniva added 1 commit 2024-10-03 01:39:01 -07:00
aniva merged commit b174b4ea79 into dev 2024-10-03 08:47:31 -07:00
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 description provided.