有没有办法将作为参数传递的函数应用于两种不同的类型？作为一个人为的例子,我可以(Maybe Int, Maybe Bool)用表达式创建一个(Just 3, Just True),但是如果我尝试使这个行为更通用的功能
generic :: (a -> Maybe a) -> (Maybe Int, Maybe Bool)
generic f = (f 3, f True)
所以我可以做类似的事情generic Just,编译器抱怨因为类型变量a是常量.
其用例是将通用函数应用于树结构,其中每个节点按类型进行参数化.
我创建了这个示例类型来演示我遇到的问题：
Inductive foo : nat -> Prop :=
| foo_1 : forall n, foo n
| foo_2 : forall n, foo n.
现在很清楚foo_1 0 <> foo_2 0，但我无法证明这一点：
Lemma bar : foo_1 0 <> foo_2 0.
Proof. unfold not. intros H. discriminate H.
这将返回错误
不是可歧视的平等。
inversion H根本不会改变上下文。奇怪的是，如果我foo从Prop改为 ，Type那么证明会通过，但我不能在我的实际代码中这样做，因为它会导致其他地方出现问题。
我怎样才能得到这个证明？为什么这首先是有问题的？