Tesla Zhang‮

Code: ```aya open data Nat | zero | suc Nat open data Vec (n : Nat) (A : Type) : Type | zero, A => vnil | suc n, A...

I think it makes sense for now to improve the idiom brackets feature and push the others until we have time

https://twitter.com/Heartof_Gold__/status/1416475517679702020 ???

I kinda understand AK's design rn. It is similar to Jesper's  approach: the `Ctx` contains a level, and the expressions are checked accordingly. In our approach, we propagate the...

We will have our own commands, can't reuse any existing ones

> Like what commands? aya-prover/aya-prover-proto#486

@re-xyr But it's no good, incompatible with other backends of Doc

> I don't quite understand. Are we doing a literate -> Doc -> output translation? Yup

> But if we use LaTeX syntax, what's incompatible with LaTeX-like -> Doc -> other format? Then we need to parse latex!

@re-xyr I think their approach is bad. We need to make our own backend generating latex.