Tesla Zhang‮

> Like when? In Arend they have `\have`. You can check it out

@re-xyr Idk but it's used a lot in the stdlib

@re-xyr I wonder which one is useful

Isn't this just https://github.com/aya-prover/aya-dev/blob/fef26881a0f9bd650dad9ada79affce5c591559d/base/src/main/java/org/aya/tyck/error/UnifyError.java#L21-L27 ?

:worried: In case of data we would also need induction-recursion..

@ice1000 Test by @ice1000

Oh geez

> > @ice1000 Test by @ice1000 > > What is this? Checkout the telegram group.

```aya open data Z : Set | zeroZ | succZ Z { | predZ n => n } | predZ Z { | succZ n => n } ```

Related: #242