The Coq mailing list

[Jasper Hugunin <jasperh AT cs.washington.edu>]

The most direct interpretation of this request would be to print

`vvv_lt_irrefl = let s := _ in let H := _ in H : forall v : vpg_var, vpg_var_as_OT.lt v v -> False`,

which is not much different from what `About` would print in this case, which is something like

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

Since sub-definitions aren't part of the global environment, there is no unfolding going on in your example. The proof term for `vv_lt_irefl` is exactly what gets printed.

Sincerely,

- Jasper Hugunin

 

  On 22/08/2020 16:43, Kumar, Ashish wrote:
> 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