Say I have the following interface in idris:
interface I a b where
x : a
y : b
And then I try to define the following function:
x' : I a b => a
x' = x
But then I get this error:
Error: While processing right hand side of x'. Can't find an implementation for I a ?b.
Main:06:6--06:7
02 | x : a
03 | y : b
04 |
05 | x' : I a b => a
06 | x' = x
^
How do I specify to idris that x
is the x from I a b
and not the x from I a ?b
?
Say I have the following interface in idris:
interface I a b where
x : a
y : b
And then I try to define the following function:
x' : I a b => a
x' = x
But then I get this error:
Error: While processing right hand side of x'. Can't find an implementation for I a ?b.
Main:06:6--06:7
02 | x : a
03 | y : b
04 |
05 | x' : I a b => a
06 | x' = x
^
How do I specify to idris that x
is the x from I a b
and not the x from I a ?b
?
1 Answer
Reset to default 1Found the answer! b
is essentially an implicit argument to x
so you can set it just like you would for a function:
x' : I a b => a
x' = x { b = b }