最新消息:雨落星辰是一个专注网站SEO优化、网站SEO诊断、搜索引擎研究、网络营销推广、网站策划运营及站长类的自媒体原创博客

How to specify the interface from which an object comes from in idris - Stack Overflow

programmeradmin4浏览0评论

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?

Share Improve this question asked Jan 17 at 20:50 דניאל פ.ח.דניאל פ.ח. 4573 silver badges8 bronze badges
Add a comment  | 

1 Answer 1

Reset to default 1

Found 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 }
发布评论

评论列表(0)

  1. 暂无评论