Tesla Zhang‮

First we need to be able to parse `\let x => 3` as an individual expression I gues

We have copatterns already, so it's about having coinduction.

Yes, but probably we should be more error tolerant? (This error is happened after a set of normal IDE operations, so it can happen to users as well)

Added error handling for this

``` java.lang.IllegalArgumentException: Too many implemented fields (expected 3): {A=a = a', contraction=Jl {A} {a} (\lam (x : A) => (=) (inv {A} {a} {a} (p a a) *> p a...

Maybe it's time to modularize Prelude?

No successful attempts so far

This is what I see:  Is that because you've fixed it?


Source code: ```arend \func wow {U : \Type} {T : U -> \Type} (A B : U) (a : T A) (b : T B) : Nat => zero \func...