Hello,
I have a case of a lemma whose Qed was unexpectedly taking 8s. After a lot of head scratching, I eventually observed that I had activated Implicit Arguments
and Contextual Implicit
and that to my surprise, I observe that the Qed takes consistently of the order of:
Implicit Arguments
onContextual Arguments
onequ_clos_sT_proper {E}%function_scope {R}%type_scope [RR]%function_scope [f x y] _ [x y] _
but that still seems crazy to me. Is it to be expected?If I understand the doc correctly, Implicit Arguments
must be on for the other related flags to take effect. Then I wonder if determining whether to make an argument implicit may involve unfolding definitions.
Yes. For instance, constant functions don't really depend on their argument, and maybe "constant" is checked up to conversion. For instance, in the next example, it seems easier to infer the argument of bar
than the argument of foo
. But Coq seems to disagree.
Set Implicit Arguments.
Set Contextual Implicit.
Definition f (x : nat) := 0.
Lemma foo x : f x = 0. reflexivity. Qed.
(*
About foo.
foo : forall {x : nat}, f x = 0
*)
Definition g (x : nat) := x - x.
Lemma bar x : g x = 0. Admitted.
(*
About bar.
bar : forall x : nat, g x = 0.
*)
maybe a variant of https://github.com/coq/coq/issues/13435
Last updated: Oct 13 2024 at 01:02 UTC