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.
There is no way to solve your problem and this was precisely the problem that gave rise to this CEP.
Thanks Theo. Ok, then live with this approximation, as the ting I project out of is
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