假设我有一个函数
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。构造函数不正交是否重要？特别是，它是否会阻碍证据搜索？