git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/test/meta002/expected
13 lines 447 B history raw
1DataDef.idr:74:1-9:
2While running an elaboration script, the following error occurred:
3Prelude.Either.Either is already defined as a datatype.
4Tacs.idr:299:15:
5When checking right hand side of testElab3 with expected type
6 DPair Ty (Tm [])
8Unifying ty and ARR ty t would lead to infinite value
9AgdaStyleReflection.idr:315:5:
10When checking right hand side of baz with expected type
11 (Nat, Void)
13PROOF SEARCH FAILURE is not defined.