Tesla Zhang‮

@lunalunaa don't forget to add a test

I think `c2` should not be legal. The args to a class should be in order, because otherwise there will be many ambiguities. Does that make things easier?

> > I think `c2` should not be legal. The args to a class should be in order, because otherwise there will be many ambiguities. Does that make things easier?...

> @ice1000 The support of any partially application brings implementation difficulties, and might not necessarily be useful, as is mentioned by kiwa I see. I'll think more about this, but...

Haskell's do notation is too simple. Maybe we need Agda's do which has the `where

Is it implemented already?

Complted

> What is neutralization by elimination? It's a meme

> Then it doesn’t sound like a plan So, I actually meant normalization by evaluation. I guess we need to add `Value` and `Neutral`, and then implement `eval`, right? I...

> We may not need to add a dedicated Neutral type even. Neutral can be a constructor for Val, consisting of a neutral head plus a spine. What kind of...