Timeline for Reasoning about CwFs in a proof assistant
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 22, 2023 at 21:26 | comment | added | Joey Eremondi | Huzzah, it works! I'll leave the question open a bit though, since I am genuinely curious how this would work in Coq or Lean. | |
| Jun 22, 2023 at 20:18 | comment | added | Joey Eremondi | Hmmm, interesting development, it looks like the problem is that I was using a relation other than the normal builtin equality. If I use e.g. HeterogeneousEquality, the example you give fails to compile. I'll see if there's an existing bug report | |
| Jun 22, 2023 at 19:58 | comment | added | Joey Eremondi |
Hmm, okay, that works better than anything I've tried so far, even if we introduce an operation foo : X -> X and rewrite by eq: foo x ≡ y. It probably shouldn't be too hard to write an elaborator reflection macro that takes a record type and re-declares each of its fields as an abstract...
|
|
| Jun 22, 2023 at 16:23 | history | answered | gallais | CC BY-SA 4.0 |