假设我有一个定义，f : x -> y -> z在那里x可以很容易地推断。因此，我选择使用做x一个隐式参数Arguments。
考虑以下示例：
Definition id : forall (S : Set), S -> S :=
fun S s => s.
Arguments id {_} s.
Check (id 1).
显然S = nat可以通过Coq进行推断，并且Coq答复：
id 1
: nat
但是，稍后，我想使隐式参数明确，例如为了可读性。
换句话说，我想要这样的东西：
Definition foo :=
id {nat} 1. (* We want to make it clear that the 2nd argument is nat*)
这有可能吗？如果是这样，什么是合适的语法？
您可以在名称前加上，@以删除所有隐式并显式提供它们：
Check @id nat 1.
您还可以使用(a:=v)通过名称传递隐式参数。这不仅可以阐明正在传递的参数，还可以让您传递某些隐式而不传递_其他参数：
Check id (S:=nat) 1.
Definition third {A B C:Type} (a:A) (b:B) (c:C) := c.
Check third (B:=nat) (A:=unit) tt 1 2.
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句