4 ms·
How do you prove to the type-checker that e.g. `append(v: [T, N], w: [T, M]) -> [T, N + M]`? Or, to make it easier, that just `append(v: [T, N], x: T]) -> [T,
by ReleaseCandidat 3y ago
How do you prove to the type-checker that e.g. `append(v: [T, N], w: [T, M]) -> [T, N + M]`?
Or, to make it easier, that just `append(v: [T, N], x: T]) -> [T, N + 1]`?
- madsbuch 3y agoyou implement the function recursively and let the compiler derive a proof by induction.