假设我有一个包含很多模块和部分的代码.在其中一些中有多态定义.
Module MyModule.
Section MyDefs.
(* Implicit. *)
Context {T: Type}.
Inductive myIndType: Type :=
| C : T -> myIndType.
End MyDefs.
End MyModule.
Module AnotherModule.
Section AnotherSection.
Context {T: Type}.
Variable P: Type -> Prop.
(* ↓↓ ↓↓ - It's pretty annoying. *)
Lemma lemma: P (@myIndType T).
End AnotherSection.
End AnotherModule.
通常Coq可以推断出类型,但我经常会输入错误.在这种情况下,您必须使用@显式指定隐式类型,这会破坏可读性.
Cannot infer the implicit parameter _ of _ whose type is “Type”.
有办法避免这种情况吗?是否可以指定默认参数之类的东西,每次Coq无法猜出类型时都会替换它们?
最佳答案 您可以使用类型类来实现默认值的概念:
Class Default (A : Type) (a : A) :=
withDefault { value : A }.
Arguments withDefault {_} {_}.
Arguments value {_} {_}.
Instance default (A : Type) (a : A) : Default A a :=
withDefault a.
Definition myNat `{dft : Default nat 3} : nat :=
value dft.
Eval cbv in myNat.
(* = 3 : nat *)
Eval cbv in (@myNat (withDefault 5)).
(* = 5 : nat *)