leanprover-community / leanprover-community/mathlib4
`apply_fun`: "internal exception: postpone"
Open
@kmill is already working on this.
Since Dec 28, 2023.
- Dominant language
- Lean
- Stars
- 4.2k
- Forks
- 1.7k
- PR merge metrics
- No merged PRs in 30d
Description
import Mathlib.Tactic.ApplyFun
example (a b : Nat) (h : a = b) : False := by
apply_fun ((·) + 1) at h
I think this is nonsense syntax, I don't understand what the (·) syntax is parsed as, but the error message definitely shouldn't be that
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.