leanprover-community / leanprover-community/repl
pattern-matching in theorem signature causes `unknown constant 'foo.match_1'`
Nobody has claimed this yet.
- Dominant language
- Lean
- Stars
- 228
- Forks
- 71
- Avg merge
- 15m
- Merged PRs (30d)
- 4
Description
{"cmd": "#eval 1 + 1"}
{"cmd": "def foo : (fun ((x, y, z) : Nat × Nat × Nat) => x = x) = fun x => True := by sorry", "env": 0}
{"tactic": "simp", "proofState": 0}
Expected: Goal closed
Actual: {"message": "Lean error:\nunknown constant 'foo.match_1'"}
This comes down to https://github.com/leanprover-community/repl/commit/66515025d9ccffa2be29718d31b816edd0675202 which eliminates both foo and foo.match_1 from the env.
I'm not sure why the InfoTree env has foo actually, but I've made a question about this on Zulip.
Contributor guide
No contributing guide indexed for this repository
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.
Research direction
Reproduce the reported REPL input using the #eval, theorem definition, and simp commands, then inspect the environment-elimination change in commit 66515025d9ccffa2be29718d31b816edd0675202. Compare the InfoTree environment with the declarations removed by that change; done means the example closes without an unknown constant 'foo.match_1' error.
Written by the indexing model from the issue text.
Assessment
- Domain
- tooling
- Issue type
- Bug
- Difficulty
- 3/5
- Estimated time
- 1-2 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 35/100