idris-0.12.3: test/reg007/expected

reg007.lidr:8:1:A.n is already defined
reg007.lidr:12:11-17:When checking right hand side of hurrah with expected type
        0 = 1

Type mismatch between
        n = lala (Type of isSame)
and
        0 = 1 (Expected type)

Specifically:
        Type mismatch between
                1
        and
                0