mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-19 09:12:34 +03:00
28 lines
687 B
Plaintext
28 lines
687 B
Plaintext
|
1/1: Building Test (Test.idr)
|
||
|
|
2/2: Building Import (Import.idr)
|
||
|
|
Error: Unknown operator '~:>'
|
||
|
|
|
||
|
|
Import:9:1--9:8
|
||
|
|
5 | (|>) : (s : HasComp x) => {0 a, b, c : x} -> a ~> b -> b ~> c -> a ~> c
|
||
|
|
6 | a |> b = comp s a b
|
||
|
|
7 |
|
||
|
|
8 | (~:>) : Type -> Type -> Type
|
||
|
|
9 | a ~:> b = Pair a b
|
||
|
|
^^^^^^^
|
||
|
|
|
||
|
|
1/3: Building Prefix (Prefix.idr)
|
||
|
|
Error: While processing right hand side of test. When unifying:
|
||
|
|
Either ((!!) a) ((!!) b)
|
||
|
|
and:
|
||
|
|
Either a ?b -> Void
|
||
|
|
Mismatch between: Either ((!!) a) ((!!) b) and Either a ?b -> Void.
|
||
|
|
|
||
|
|
Prefix:12:17--12:27
|
||
|
|
08 | (!!) = Not
|
||
|
|
09 |
|
||
|
|
10 | export
|
||
|
|
11 | test : Either (!! a) (!! b) -> !! (a, b)
|
||
|
|
12 | test f (x, y) = f (Left x)
|
||
|
|
^^^^^^^^^^
|
||
|
|
|