Timeline for Coq produce instance of a type `{x : T | P x}` inside an explicit definition given an `x'` of type `T`
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 1, 2022 at 3:41 | vote | accept | Greg Nisbet | ||
| Feb 28, 2022 at 12:07 | answer | added | Andrej Bauer | timeline score: 1 | |
| Feb 28, 2022 at 11:09 | answer | added | Meven Lennon-Bertrand♦ | timeline score: 3 | |
| Feb 28, 2022 at 4:52 | history | asked | Greg Nisbet | CC BY-SA 4.0 |