coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "Kumar, Ashish" <azk640 AT psu.edu>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] How can I print definitions without unfolding the sub-definitions within it?
Date: Sat, 22 Aug 2020 12:58:43 +0000
Accept-language: en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=psu.edu; dmarc=pass action=none header.from=psu.edu; dkim=pass header.d=psu.edu; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=rbyJJs6IouBvMvUMW2W3Ix13fa688GoGKxtFPOha/8U=; b=gafhV2XHweLIJ3HsPQkclHALiy0oo3Nxk42gvCrR5so3yRmDQkoTcF0OZ+gdUz/RyrlLkvmrSN23rYUxq9wPaTu77wvIDUsL4lhxm0YPo0q6Pz/qbBWWJOBJVbuSPkIWavnvJllysxFxekOw2KnAWu7hEjVlzD7JtQLT8gIhqtHC+DL1GTg3Aqd+vnU2LuI2YWTy51AtciFOoLhg2vew0GVPWDUjo6tozLj3m0kbhG/NuT2ZZ0h1UXv1bhyiJEYr+TZAgbN+d5LtmU7MOpUs0Si/V10aldrAs7U8K6bFOf6RbvuazSIyBBfnIV4/pdER0CsGxHZUScmVki6xmcv7Kg==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=E3ac6qTGH5eAXAduuuR9qUzrRpyMInCuZbJYdO5zGbzFehYm3M/a1NNXbQDkLkkeNRlSMpxcUyXA7993AX4b1x83n3+Jr10uaMrFssFqQRdU1ahWR03f0K6UDz4pV3viEKHRgk90kK/5GQIQP+MKcpaOmbawBvNJ4JIOYSSYsdiL+lcS2246MzW/Rhxnr6gor3bCjFmGsSvV0di4LD1vw3bwi/3oi8P4kFqF6XCglsTEctTa9IZdC7X8V1SHiOtAqOGVVUgwVeaCOibr5pUeqsF5yH8TLeMv+nQYcGDhAxz2f3Tm4DTRC2VTfjua/sOmj8JMPVABQevEKNpoTyw3zQ==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=azk640 AT psu.edu; spf=None smtp.mailfrom=azk640 AT psu.edu; spf=Pass smtp.helo=postmaster AT NAM10-DM6-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:ex0QBxEb80SSEYOsdQr7Ap1GYnF86YWxBRYc798ds5kLTJ7zrsmwAkXT6L1XgUPTWs2DsrQY0rSQ6vm8EjFeqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5zIRmssAndq8YbjYRiJ6sw1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrhK/qRJi347aboKbNPticazSZt4VX3ZNUtpLWiBdHo+wco0CBPcBM+ZCqIn9okMDoRW7CwmxAePg0CVIimfr1qAmyOQhEQDG3BcgH94ArX/Zq8/6NaYRUe20w6TE0S7Ob+tN2Tfg8oTHbA0uoeyVUL92bMHexlUhGRnfgVWMtYzqISmV1uIVvmab7+dtVeaih3AmpgxyvDShycUhhIbGiIwa113J9CF0zYkrKdClVUN2YNCpHZlMuy+UOYV7TMAvT3x2tCsk17ELv4OwcisSyJk/yBPTd+aLf5WU7h/hTuqcJTl1iGh4dL+xhRu+6VWsxvHzW8Wu3ltHrTBJn9bSunwX1hHf99CLRuV880u91zuC0h3f5v1fLk01kKfXNYItz701m5cTtUnOGyr7lFjrgKKQa04q4PKn6/79bbXjvpKcN5F7igX5Mqk2gsKyHeM2PhUSU2SC9+qy07zu8VT+QLpRkPI6iK7ZsI3GJcsAoa65HglV3Zs55xanFTem18gYkmcbI1JZeRKHiI7pN0vJIPDlEfe/h1OskDBox/zcIrLhBZDNImDCkLfnY7l991ZRxQUvwdxF+p5YFrMMLOj3V0L/rtDUExE0Pg6sz+biEtp914ceWWyVAq+eNaPfqUWH5+MsI+SNa4IZpC3wK+A+5/7zl3M2h0ISfbSx0ZsNdH+4BuhmI1meYXf0ntgBFn4KshMiQ+zulV2NSiVeZ22yXqI5/jE0EpiqDYbFRoC3gbyOxj23HpNMZjMONlfZGnDxMo6ARv1EPCmVO4pqliEOfbmnUY4okx+04lzU0b1ie6D35ygRr9ar/cN15vbT31lm/C53UZjF+3mWUid5kn5eFGx+57x2vUEokgTL6qN/mfENTYUPtcMMaR8zMNvn98I/E8r7C1DZZcrPRVq7EI3/UGMBC+kpytpLWH5TXtCrjxTNxS2vUu0NjKHNCZApoPqFgirBYv1lwnOD75EPylkrRswTaj+Ar4smr03/ItCMlE+U0aG3aa4bwSjBsn+ZynaDt11ZVwg2VrjZWXcYZQ3dqtGrv04=

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