Timeline for What are the main differences between Coq and Lean?
Current License: CC BY-SA 4.0
18 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 13, 2023 at 23:52 | comment | added | Kyle Lin | @SebastianUllrich Regarding #4, how can you encode Coq-like non-uniform parameters using (uniform) parameters and indices? If you would link an example, I'd really appreciate it. | |
| Mar 1, 2022 at 13:36 | comment | added | Jason Rute | “I'll leave summarizing the ‘setoid hell’ discussion to someone else...” proofassistants.stackexchange.com/questions/908/… | |
| Feb 18, 2022 at 15:10 | comment | added | Sebastian Ullrich | @MarioCarneiro Whoops, fixed! | |
| Feb 18, 2022 at 15:10 | history | edited | Sebastian Ullrich | CC BY-SA 4.0 |
typo
|
| Feb 13, 2022 at 17:06 | vote | accept | Ricky | ||
| Feb 9, 2022 at 22:31 | comment | added | Sebastian Ullrich | @darijgrinberg What exactly are you objecting to? Both systems have LEM in their stdlib. Whether you use it is mostly a question of social norm, as described in Jason's answer. | |
| Feb 9, 2022 at 21:34 | comment | added | darij grinberg | "The set of axioms is quite different in both systems, but propositionally equivalent." Huh? I thought Lean was non-constructive by design. | |
| Feb 9, 2022 at 14:47 | comment | added | Sebastian Ullrich | @palmskog Interesting! Feel free to suggest edits. (Should I turn this answer into a community wiki?) | |
| Feb 9, 2022 at 14:31 | comment | added | palmskog | Coq users that use the Equations plugin will have their definitions compiled down to eliminators for inductive types, equality and accessibility. This is very close to Lean's "fundamental recursor functions", and essentially means that one does not have to trust Coq's guard condition. | |
| Feb 9, 2022 at 13:45 | comment | added | Sebastian Ullrich | @MevenLennon-Bertrand Thanks, added. By "indeterminate" I meant universe variables, basically. | |
| Feb 9, 2022 at 13:44 | history | edited | Sebastian Ullrich | CC BY-SA 4.0 |
clarified universe polymorphism
|
| Feb 9, 2022 at 13:36 | comment | added | Sebastian Ullrich | @NeelKrishnaswami mutual inductives themselves were never absent afair. What was missing until very recently is frontend support for well-founded recursion, without which you would have to use the mutual recursor directly. github.com/leanprover/lean4/blob/master/tests/lean/run/… (yes, linarith would really help here) | |
| Feb 9, 2022 at 13:11 | comment | added | Meven Lennon-Bertrand♦ | What do you mean by "concrete but possibly indeterminate"? Coq also has support for universe polymorphism these days. | |
| Feb 9, 2022 at 11:46 | comment | added | Neel Krishnaswami | Hi! Do you have a link to any documentation of Lean 4's mutual inductives? My PhD student says it doesn't support it yet, and he would be over the moon to learn he is wrong. :) | |
| Feb 9, 2022 at 9:41 | history | edited | Sebastian Ullrich | CC BY-SA 4.0 |
clarified inductive signatures part
|
| S Feb 9, 2022 at 9:40 | history | suggested | Glorfindel | CC BY-SA 4.0 |
typo corrected
|
| Feb 9, 2022 at 9:40 | review | Suggested edits | |||
| S Feb 9, 2022 at 9:40 | |||||
| Feb 9, 2022 at 9:38 | history | answered | Sebastian Ullrich | CC BY-SA 4.0 |