cstolze

Inferring implicit parameters of binders is too slow

1

The following code takes 0.4 seconds to get typechecked: ``` constant symbol T : TYPE; constant symbol τ : T → TYPE; constant symbol A : T; constant symbol U...

Custom binders do not allow for multiple variables at once: ``` constant symbol U : TYPE; constant symbol ∀ : (U → U) → U; notation ∀ quantifier; symbol foo...