Timeline for Rules about Prop and Set in UTT
Current License: CC BY-SA 3.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 11, 2014 at 19:13 | comment | added | Konstantin Solomatov | Basically, I want to understand tradeoffs which we have when we design dependently typed language, to implement one myself (I already implemented a language which is similar to what you implemented in your blog but with inductive types). I am doing this, since I want to apply projectional editors, the thing which I am working at JetBrains, to dependent types and I feel that it's the area where they are currently most useful. Since the length of the comment is limited I will write you email, where I explain this in more detail. | |
| May 11, 2014 at 16:18 | comment | added | Andrej Bauer | May I ask why you're learning this stuff? | |
| May 11, 2014 at 15:48 | comment | added | Konstantin Solomatov | Thank you very much! I can't imagine how I would find this out without your answer (and learn dep types without your other answers here). | |
| May 11, 2014 at 15:48 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
added 1 character in body
|
| May 11, 2014 at 15:42 | vote | accept | Konstantin Solomatov | ||
| May 11, 2014 at 7:39 | history | answered | Andrej Bauer | CC BY-SA 3.0 |