The Coq mailing list

[Li-yao Xia <lysxia AT gmail.com>]

There could be an attribute for this.

One hacky solution is to start from the normal, transparent definition, and use it in a separate Qed-ed Definition which also extracts the type from it. The initial definition can be erased by making it local to a section:

Notation type_of x := ltac:(let t := type of x in exact t) (only parsing).

Section FOO.
Let foo_ := 3.
Definition foo : type_of foo_.
Proof. exact foo_. Qed.
End FOO.

Cheers,
Li-yao

On 2022-06-02 1:19 AM, mukesh tiwari wrote:

Hi Qinshi,

I am not sure if it's exactly going to solve your problem, but have a look at the locking and unlocking mechanism in math-comp [1, 2, 3]. 

Best,

Mukesh

[1] https://github.com/math-comp/hierarchy-builder/wiki/Locking

[2] https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/matrix.v#L282-L283

[3] https://coq.inria.fr/distrib/V8.14.0/stdlib//Coq.ssr.ssreflect.html#locked_with

On Wed, 1 Jun 2022 at 22:11, Qinshi Wang <qinshiw AT cs.princeton.edu> wrote:

Hi everyone,

Is there any way to make a "Definition" as opaque as a proof ended with "Qed"? My use case is I want to specialize a lemma and define

Definition foo := lem (* a lot of paramters *).

I want to omit its type, which is long. So I cannot start a "Proof." in a normal way.

Thanks,

Qinshi