Closed jakzale closed 4 years ago
Similar to #33, but for general type ascriptions in the code, of the form:
M : U
for some expression M and some type U.
M
U
Related to #33, as both deal with having universes/types available in the language.
Similar to #33, but for general type ascriptions in the code, of the form:
for some expression
M
and some typeU
.