valis

I saw it too, but I cannot reproduce it stably.

Do you want to write `x.v` or just `v`? The title of the issue makes me think that you want the latter, but the text itself has the former option.

It's hard to tell what's causing this problem, but a few days ago I found and fixed a bug related to patterns. I think it might cause this exception, but...

Actually, I have some a list of sets that can be added Arrows 2190-21FF Leterlike Symbols 2100-214F Miscellaneous Methematical Symbols_A 27C0-27EF Suplemental Arrows_A 27F0-27FF Suplemental Arrows_B 2900-297F Miscellaneous Methematical Symbols_B...

No technical problems, I just don't want this feature to be abused by using some extremely weird symbols.

This is an expected behavior because the type of a function defined by pattern matching is checked before the body, but the type of the first version is checked together...

Actually, we can defer the inference of levels for the type in the second version.

No. It is still easy to get stack overflow. I'm going to fix this, but it still makes sense to implement a separate evaluator (or even compiler) for closed expressions.

It is an individual expression. It's equivalent to `\let x => 3 \in {?}`.

I think it's caused by broken bin files.