Commit 2024-03-15 22:49 1a1dffdd
View on Github →chore: fix extract_lets without at (#11400)
Make extract_lets (without any specified at) work on just the goal. This supplements the already valid syntax extract_lets at h ⊢ and extract_lets at *