Tesla Zhang‮

The problem is that there isn't a reliable tree-sitter implementation for JVM. IIRC fleet uses their own binding, which I consider reliable, but it's not open sourced

That's cool! I also wish to see how compiled hoas would compete to other languages and runtimes 😲

> by using `-v ERROR` ? A specific warning, like `@Suppress ("Bla")`. We may use the fqname of a problem class as its id

`suc-suc-a` should be evaluated to `suc (suc a)` and it corresponds to the pattern of the same form.

```aya \pat fail (a, b : Nat) => addN b a ``` Stuck application should fail to be a pattern object, so the above code should fail.

> Can we write \impossible in pattern functions? Will it be able to be used as an ordinary function then? Interesting question! I think we don't have to. Reason: if...

During Walpurgis night, we decide to go to Arend style `let`

We think modules in let being to complicated

+ :+1: for having local modules + :-1: for simple `let` like in Arend @re-xyr is not allowed to cast vote

Sometimes we want let bindings to be irreducible within the body (and only reduce when applied)