coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How can I print definitions without unfolding the sub-definitions within it?

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How can I print definitions without unfolding the sub-definitions within it?
Date: Sat, 22 Aug 2020 15:38:45 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay6-d.mail.gandi.net
Ironport-phdr: 9a23:tUYx3hRjjvwnUZ2SrrA1AVVsC9psv+yvbD5Q0YIujvd0So/mwa6ybBCN2/xhgRfzUJnB7Loc0qyK6v6mADVcqsjY+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi3oAnLq8UanIRvJqkwxxfUv3BFZ/lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/WfKgcJyka1bugqsqQFhzY7aYI+bN/Rwca3SctwYWWVPUd1cVzBCD46mc4cDE+QMMOZeooLgp1UOtxy+BQy0Ce3u0DBPmmP20rc80+s5EA/G3QggEMkQv3TOsNX+KaAfUe+vw6bW0TXMdfVW1S3y6IjJdhAuuu+DXahsccfK0kkvFAPEjk6TqYzkOjOV0/oCs3KB4+pmS+2vl3cqpgdsqTeg2skikJPGhp4Jyl/a7yV5xp44KNm8RUN/fdKqH5RduS6GO4Z0Tc0uX25ltDs6xLAJpZK2czQHxZAmyhPRZPKKboqF7BzsWuuMPzp1gG5pdb2hihu07EOuyfX8W9Gq3FpXrCdJiNvBumwX2xDO6cWKROFx8lql1DuMzwzf9/1ILEQumabFJZMt3KQ8moQNvUnBBCP6hUr7gauQe0454Oan8f7nba/jppKEN497lAX+MqM2l8ylH+s4NhIBXmia9OilybLv50j5T69Ljv0yiKXZv4rVJcIGqa64GQNV1Jgs6wqnAzen1tQXg2UHIUpbdB6ajYXlIVPDLOziAfuigFmhni1ny+3CM7DiGpnNK2LMkLblfbZz8U5czw8zwMhQ551OFL4BPOj8WknruNzXDx85Nxe7zPj9CNVhzY4eQmGPA6+CMKPRsF+I4+cvLPeWZIMPvjbyNeQl6+b0jXAlgV8dYbWp3ZwPZX+kGfRmOlyVbmbogtccCmgHpRE+TezviF2aSzFffXeyX6Qm5jE6Eo2qF4nDRpr+yICGiSy8B9hdYn1MIlGKC3bhMYueCNkWbyfHDcbijjUCYpegT4Uszw3m4ADzxqZuKKzb+ykSuIj//MN29vbQlBQ3+CYyCcmBhTLeB1pol38FEmdllJt0plZwnw/ajfpIxsdAHNkW3MtnFx8gPMeCnfd5GsvxWwfEc83PTlu6EI3/UGMBC+kpytpLWH5TXtCrjxTNxS2vWuFHjL+aH58196fRxT73Ktovki+bhplktEEvR450DUPjhqN78FKOVZTEl0yIyeOmM6EV3SqL+26FwWvIukxEAlZ9

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

[Coq-Club] How can I print definitions without unfolding the sub-definitions within it?, Kumar, Ashish, 08/22/2020
- Re: [Coq-Club] How can I print definitions without unfolding the sub-definitions within it?, Gaëtan Gilbert, 08/22/2020
  - Re: [Coq-Club] How can I print definitions without unfolding the sub-definitions within it?, Kumar, Ashish, 08/22/2020
    - Re: [Coq-Club] How can I print definitions without unfolding the sub-definitions within it?, Gaëtan Gilbert, 08/22/2020
      - Re: [Coq-Club] How can I print definitions without unfolding the sub-definitions within it?, Jasper Hugunin, 08/22/2020
        
        Re: [Coq-Club] How can I print definitions without unfolding the sub-definitions within it?, Gaëtan Gilbert, 08/22/2020