Tesla Zhang
Tesla Zhang
I just wanna point out one thing -- the order of overwriting should matter. Say, if you wanna overwrite a field, you gotta override it before new fields got added.
```aya \struct Monoid | A : \Set | \pattern identity : A | \infix + (a b : A) : A \with { | identity, a => a | a,...
https://github.com/JetBrains/arend-lib/blob/7d2f65b380ed9787963a0c7f9339ec6d8e17d1cb/src/Homotopy/Torus.ard
I want pattern synonym to be a first-class citizen in the language. We need to have a type for them.
```aya \struct Monoid | A : \Set | \pattern identity (x : A) : A | \infix + (a b : A) : A \with { | identity x, a...
We could start from 'pattern definitions': ```aya \pat one : Nat => suc zero \pat suc-suc-a (a : Nat) => suc (suc a) \def a-2 (a : Nat) : Nat...
> We might need a more precise definition of "subtyping." For now, I would define coercion as "functions that are implicitly inserted during elabration to make things tyck." Totally agreed...
> Does Arend coercion allow coercing a type with parameters, like \all {A} {n : Nat} -> Vec A n -> List A? I don't know. I wish we could...
> Like rust's `Into`? Yes, and we builtin this thingy.