coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] exact tactic vs Definition

From: Frédéric Blanqui <frederic.blanqui AT inria.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] exact tactic vs Definition
Date: Wed, 28 Dec 2022 10:26:22 +0100
Authentication-results: mail3-relais-sop.national.inria.fr; dkim=none (message not signed) header.i=none; spf=SoftFail smtp.mailfrom=frederic.blanqui AT inria.fr; dmarc=fail (p=none dis=none) d=inria.fr

Hello.

It seems that

(1) Definition f : A := t.

is faster to check than

(2) Lemma f : A. Proof. exact (t). Qed.

Is there a variant of the Definition command which is semantically equivalent to (2), that is, with f considered as a constant by the reduction/conversion engine of the Coq kernel?

Frédéric.

[Coq-Club] exact tactic vs Definition, Frédéric Blanqui, 12/28/2022
- <Possible follow-up(s)>
- Re: [Coq-Club] exact tactic vs Definition, Théo Zimmermann, 12/28/2022
  - Re: [Coq-Club] exact tactic vs Definition, Gaëtan Gilbert, 12/28/2022