mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-21 05:57:38 +03:00
14 lines
447 B
Plaintext
14 lines
447 B
Plaintext
DataDef.idr:72:1-9:
|
|
While running an elaboration script, the following error occurred:
|
|
Prelude.Either.Either is already defined as a datatype.
|
|
Tacs.idr:298:15:
|
|
When checking right hand side of testElab3 with expected type
|
|
DPair Ty (Tm [])
|
|
|
|
Unifying ty and ARR ty t would lead to infinite value
|
|
AgdaStyleReflection.idr:321:5:
|
|
When checking right hand side of baz with expected type
|
|
(Nat, Void)
|
|
|
|
PROOF SEARCH FAILURE is not defined.
|