Open fmease opened 3 years ago
If syntactically unambiguous, copy Lean's (EXPR : TYPE).
(EXPR : TYPE)
Actually, now with pi types being prefixed with For, there no longer is any ambiguity. We can simply go for EXPR : TYPE and yeet core's the :)
For
EXPR : TYPE
core
the
If syntactically unambiguous, copy Lean's
(EXPR : TYPE)
.