idris-0.9.19: test/reg007/expected
reg007.lidr:8:1:A.n is already defined
reg007.lidr:12:11-17:When checking right hand side of hurrah:
Type mismatch between
n = lala (Type of isSame)
and
0 = 1 (Expected type)
Specifically:
Type mismatch between
1
and
0