如何解决如果证明是正交的,这有帮助吗?
假设我有一个函数
f : Vect m Nat -> Vect n Nat -> {auto _ : Proof m n} -> Foo m n
哪里
data Proof : Nat -> Nat -> Type where
Eq : Proof x x
One : Proof 1 _
我可以将 Proof 1 1
设为 Eq
或 One
。因此,这些不是“正交”。在更复杂的示例中,我可以使用递归数据构造函数,我可以在其中提供证明为 Constructor1 Constructor2
或 Constructor3 Constructor1
。构造函数不正交是否重要?特别是,它是否会阻碍证据搜索?
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。