如何解决构造函数中的表达式时“MkFoo 的返回类型必须在 Foo 中”
我想编写一个在类型中使用表达式的构造函数。我试过了
interface FooLike ty where
metadata : (Nat,Type)
data Foo : Nat -> Type -> Type where
MkFoo : {ty : Type} -> FooLike ty =>
ty -> let (r,t) = metadata {ty=ty} in Foo r t
foo : {ty : Type} -> FooLike ty =>
ty -> let (r,t) = metadata' {ty=ty} in Foo r t
但是对于构造函数(不是函数)我得到
Return type of MyMod.MkFoo must be in MyMod.Foo
我做错了什么?
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。