Fabian Kunze (Nov 16 2020 at 09:40): Fabian Kunze (Nov 16 2020 at 09:40):What's a way to declare a lemma by giving a proof term such that the lemma is Opaque, without giving the type of t explicitly?
This fails, as Lemma expects a type:
Definition SpecT__step := projT2 SpecT__step'.
This fails, although I think I read about this somewhere, but maybe it was a Coq Improvement proposal:
#[opaque]
Definition SpecT__step := projT2 SpecT__step'.
Indeed, it is coq/ceps#42.
Théo Zimmermann (Nov 16 2020 at 09:42):There is no way to solve your problem and this was precisely the problem that gave rise to this CEP.
Fabian Kunze (Nov 16 2020 at 10:00):Thanks Theo. Ok, then live with this approximation, as the ting I project out of is Qed.-opaque:
Definition SpecT := projT2 SpecT'.
Opaque SpecT__step.
Actually, here is a possible (complicated) workaround. Example where I define an opaque bar of value 0 without ever providing its type:
Definition foo := 0.
Definition bar : (ltac:(let t := type of foo in exact t)).
exact foo.
Qed.
Oh, right, everything is possible in a world with inline-ltac :)
Last updated: Sep 30 2023 at 05:01 UTC