mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-22 03:01:31 +03:00
43 lines
1.1 KiB
Plaintext
43 lines
1.1 KiB
Plaintext
1/2: Building NoRegression (NoRegression.idr)
|
|
2/2: Building Lambda (Lambda.idr)
|
|
Error: While processing right hand side of term. When unifying Term ?g (TyFunc ?tyA (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat TyNat)))))))) and Term Empty (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat TyNat))))))).
|
|
Mismatch between: TyFunc TyNat TyNat and TyNat.
|
|
|
|
Lambda:62:3--88:9
|
|
62 | Func
|
|
63 | (Func
|
|
64 | (Func
|
|
65 | (Func
|
|
66 | (Func
|
|
67 | (Func
|
|
|
|
1/1: Building Bad1 (Bad1.idr)
|
|
Error: Couldn't parse declaration.
|
|
|
|
Bad1:3:1--3:2
|
|
1 | module Bad1
|
|
2 |
|
|
3 | data Bad = BadDCon (x : Nat)
|
|
^
|
|
|
|
1/1: Building Bad2 (Bad2.idr)
|
|
Error: Couldn't parse any alternatives:
|
|
1: Expected 'case', 'if', 'do', application or operator expression.
|
|
|
|
Bad2:3:13--3:14
|
|
1 | module Bad2
|
|
2 |
|
|
3 | badReturn : (whatever : Int)
|
|
^
|
|
... (53 others)
|
|
1/1: Building Bad3 (Bad3.idr)
|
|
Error: Couldn't parse declaration.
|
|
|
|
Bad3:4:1--4:2
|
|
1 | module Bad3
|
|
2 |
|
|
3 | badExpr : ()
|
|
4 | badExpr (whatever : ())
|
|
^
|
|
|