在接受函数的接口中约束函数参数的语法是什么？我试过：
interface Num a => Color (f : a -> Type) where
defs...
但它说Name a is not bound in interface...
Your interface实际上有两个参数：a and f. But f应该足以选择一个implementation:
interface Num a => Color (a : Type) (f : a -> Type) | f where
f这里被称为确定参数 http://docs.idris-lang.org/en/latest/tutorial/interfaces.html#determining-parameters.
这是一个无意义的完整示例：
import Data.Fin
interface Num a => Color (a : Type) (f : a -> Type) | f where
foo : (x : a) -> f (1 + x)
Color Nat Fin where
foo _ = FZ
x : Fin 6
x = foo {f = Fin} 5
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
