erg/tests/should_ok/dependent.er
Shunsuke Shibayama 0840d9bf60 fix: subtyping bug
2023-06-10 11:16:30 +09:00

5 lines
147 B
Python

concat|T: Type, M: Nat, N: Nat|(l: [T; M], r: [T; N]): [T; M + N] = l + r
l = concat [1, 2, 3], [4, 5, 6]
_ = l[5]
assert l == [1, 2, 3, 4, 5, 6]