Timeline for Found type UU where "?T" was expected
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 22, 2022 at 12:22 | history | edited | Tempestas Ludi | CC BY-SA 4.0 |
Add a link to the full exercise file
|
| Apr 22, 2022 at 12:21 | vote | accept | Tempestas Ludi | ||
| Apr 21, 2022 at 8:14 | comment | added | Tempestas Ludi |
The first one is fine, but the second one gives an error The term "∅" has type "UU" while it is expected to have type "Type" (universe inconsistency: Cannot enforce UU.u0 <= Spartan_exercises.9 because Spartan_exercises.9 < UU.u0).
|
|
| Apr 20, 2022 at 14:39 | answer | added | Jason Gross | timeline score: 3 | |
| Apr 20, 2022 at 14:39 | comment | added | Jason Gross |
What if you do simple refine (tpair _ _ _) and then refine empty in the first goal? Do either of these give error messages?
|
|
| Apr 19, 2022 at 16:28 | history | edited | Tempestas Ludi | CC BY-SA 4.0 |
added 5 characters in body
|
| Apr 19, 2022 at 11:21 | history | asked | Tempestas Ludi | CC BY-SA 4.0 |