Timeline for What does the "motive is not type correct" error mean in Lean?
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 18, 2022 at 13:20 | comment | added | It'sNotALie. |
I couldn't find a good example of this, but I have also judiciously used ▸ for this; instead of the rws as I usually would, I'd do replace old_id : (exact_term_I_want) := h ▸old_id; really tedious but it works well. For the goal, I guess you can use change_to in a similar way.
|
|
| Mar 18, 2022 at 12:39 | vote | accept | Ricky | ||
| Mar 17, 2022 at 16:08 | history | edited | Joachim Breitner | CC BY-SA 4.0 |
added 119 characters in body
|
| Mar 17, 2022 at 16:06 | comment | added | Joachim Breitner |
Ah, right, you suggested that. I’ll add it. What I find surprising: Why does simp only not complain about hx not being a suitable simplification lemma?
|
|
| Mar 16, 2022 at 23:38 | comment | added | Eric |
Does simp only [hx] {single_pass := tt} avoid the shortcomings of simp_rw hx?
|
|
| Mar 16, 2022 at 23:12 | history | edited | Joachim Breitner | CC BY-SA 4.0 |
added 295 characters in body
|
| Mar 16, 2022 at 21:26 | comment | added | Joachim Breitner | Is that a universally applicable workaround, or something that works sometimes? | |
| Mar 16, 2022 at 21:07 | comment | added | Junyan Xu |
revert h1, rw hx also works in this case :)
|
|
| Mar 16, 2022 at 12:19 | history | answered | Joachim Breitner | CC BY-SA 4.0 |