git.iko.soy/Idris-dev
on 54e4e41 help sign in
Idris-dev/test/reg007/expected
12 lines 284 B history raw
1reg007.lidr:8:1:A.n is already defined
2reg007.lidr:12:11-17:When checking right hand side of hurrah:
3Type mismatch between
4 n = lala (Type of isSame)
5and
6 0 = 1 (Expected type)
8Specifically:
9 Type mismatch between
10 1
11 and
12 0