Timeline for Comparing indexed induction to recursion
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 7 at 10:06 | comment | added | Andrej Bauer | Right, so this questionis about hacking then. | |
| Feb 6 at 21:13 | comment | added | Mike Shulman |
@AndrejBauer Yes, about judgmental equality, but in some cases I think about the even finer "syntactic equality", when it gets into waters like the behavior of simpl and typeclass inference, which do not always treat even judgmental equality 100% transparently.
|
|
| Feb 5 at 11:10 | answer | added | Meven Lennon-Bertrand♦ | timeline score: 1 | |
| Feb 5 at 7:17 | comment | added | Andrej Bauer | Assuming that is the case, the question is "about judgmental equality", it seems. | |
| Feb 5 at 5:27 | history | edited | Mike Shulman | CC BY-SA 4.0 |
clarify "types of indices"
|
| Feb 5 at 5:27 | comment | added | Mike Shulman | @AndrejBauer I don't know of a formal theorem saying that they are, but I would expect so. | |
| Feb 4 at 9:25 | history | became hot network question | |||
| Feb 4 at 7:38 | comment | added | Andrej Bauer | Out of curiosity, are the two approaches equivalent, mathematically speaking? (Let's say we limit attention to initial algebras of polynomial functors with parameters.) | |
| Feb 4 at 7:04 | comment | added | Mike Shulman | @JasonRute It's certainly closely related, but a lot of the answers to that question focus on what you can do with inductive families and not with recursive ones, whereas I'm specifically asking about how they differ in the case when you can do both. | |
| Feb 4 at 5:39 | comment | added | Jason Rute | This this a duplicate of this question? proofassistants.stackexchange.com/questions/2136/… | |
| Feb 4 at 2:54 | answer | added | Hiroki Chen | timeline score: 1 | |
| Feb 4 at 1:23 | history | asked | Mike Shulman | CC BY-SA 4.0 |