假设我有一个函数
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
.构造函数不正交有关系吗?特别是,它是否妨碍证据检索?
