The Coq mailing list

["Kumar, Ashish" <azk640 AT psu.edu>]

Here's one example I could find (not the worst one, but it highlights my point):
In one of the files in my project 'vv_lt_irefl' is a lemma defined by:

    Lemma vv_lt_irefl : forall (v:vpg_var),        vpg_var_as_OT.lt v v -> False.

When I encountered the term 'vv_lt_irefl' in another file for the first time, I did 'Print vv_lt_irfl'. Coq's output was:

vv_lt_irefl =

let s : StrictOrder vpg_var_as_OT.lt := vpg_var_as_OT.lt_strorder in

let H : forall v : vpg_var, vpg_var_as_OT.lt v v -> False :=

  match s with

  | {| StrictOrder_Irreflexive := StrictOrder_Irreflexive;

    StrictOrder_Transitive := StrictOrder_Transitive |} =>

      (fun (StrictOrder_Irreflexive0 : Irreflexive vpg_var_as_OT.lt)

         (_ : Transitive vpg_var_as_OT.lt) (v : vpg_var) =>

       let c : complement vpg_var_as_OT.lt v v := StrictOrder_Irreflexive0 v in

       c) StrictOrder_Irreflexive StrictOrder_Transitive

  end in

H

     : forall v : vpg_var, vpg_var_as_OT.lt v v -> False

It clearly unfolded the term 'vpg_var_as_OT.lt', and even unfolded terms within this term - making it hard to read. Is there a way I can print 'vv_lt_irefl' without Coq unfolding it's inner terms?

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
Sent: Saturday, August 22, 2020 9:38 AM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] How can I print definitions without unfolding the sub-definitions within it?

 

Depending on what you mean by "sub definitions" this may be impossible. Can you give an example?

Gaëtan Gilbert

On 22/08/2020 14:58, Kumar, Ashish wrote:
> I use "Print A" to print the definition of a term A. But Coq unfolds all the sub-definitions and functions within the term and sometimes, the resultant definition becomes very long and unreadable. Is there a way by which I can print definitions without having Coq unfold the inner functions and definitions? (I tried set unprinting notations, but that didn't work).
>
> With regards,
> Ashish