For the example
sum(n :: #, Vec(Int, n)) -> Int
sum(_, []) = 0
sum(1, x ,- []) = x
sum(_, xs =,= ys) = sum(!, xs) + sum(!, ys)
sum(_, xs =, m ,= ys) = sum(!, xs) + m + sum(!, ys)
I get
Error in examples/match.brat:
Internal error: Redefining In match_check_defs_1_sum_LambdaChk_7_checkClauses_1_$lhs_27_typeEqsTail_5_gen_1_Div_3 0
Hint: if I explicitly match on n in the last case, there's no error
sum(n :: #, Vec(Int, n)) -> Int
sum(_, []) = 0
sum(1, x ,- []) = x
sum(_, xs =,= ys) = sum(!, xs) + sum(!, ys)
sum(succ(_), xs =, m ,= ys) = sum(!, xs) + m + sum(!, ys)
For the example
I get
Hint: if I explicitly match on
nin the last case, there's no error