Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Definition as opaque as Qed

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Definition as opaque as Qed


Chronological Thread 
  • From: Qinshi Wang <qinshiw AT cs.princeton.edu>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Definition as opaque as Qed
  • Date: Wed, 1 Jun 2022 17:10:56 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=qinshiw AT cs.princeton.edu; spf=Pass smtp.mailfrom=qinshiw AT cs.princeton.edu; spf=Pass smtp.helo=postmaster AT violeteyes.cs.princeton.edu
  • Ironport-data: A9a23:paExYKjk4MwH89XAuMge5ASlX161uRYKZh0ujC45NGQN5FlHY01je htvWTrTPf6Pa2r9Lttwa43lpxgCv8eAyNE2S1M5/iw0ESNjpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UKieUsxIbVcMpB0J0HqPoMZkxN8x6TSFK1nV4 4mq/ZWGYATNNwNcawr41YrT8HuDg9yp4Fv0jnRmDRyclAK2e9E9VfrzFInpR5fKatE88t2SG 44v+IqEElbxpH/BPD8KfoHTKSXmSpaKVeSHZ+E/t6KK2nCurQRquko32WZ1hUp/0120c95NJ NplkqG6YloCOJP3kt8sb0ljQytQGu4YweqSSZS/mZT7I0zubXrrx/hyAVA7JssT4aBvG2BI/ vEELzZLYxye7w606OvhGq81355ldZK1et5C0p1j5Wmx4fIOWJHFWKXL+vdTx3EonMFIFvvCY MxfZDZyBPjFS0QSZAhPWc1m9AuurlPFURx1qlKrnpBt6GrN5zNd9rHwGvOAL7RmQu0IzhfD/ j+uE37CKhodLZmUzSeP2mm9g/fG2yL9QoMbUrOinsOGm3WNx2sXBQEbRFag5/KizFakWtRUJ lAT/GwjobVaGFGXosfVeCCyiyOvuCAnUeFhL70BuAuj7emK2lPMboQbdQJpZNsjvc4wYDUl0 F6Vgt/kbQBSXK2ppWG1qu/P8GjqUcQBBSpdOXFZEVJtD8zL+dlbs/7Zcjp0/EdZZPXNAzD2y D2Wqy5Wa1471Z5Wi/nTEbzvpT+z7rrEVBU4923qso+N8AJ+YIO5ap2l8h7Q9rBYNoefRVSdu 35ClsSDhAzvMX1vvHDcKAnuNOj3jxpgDNE6qQQ+d3XG327zk0NPhagKvFlDyL5Ba67ogwPBb k7Joh9275ROJnasZqIfS9vvVphzlfi6Toi8DKC8gj9yjn5ZKFHvEMZGORP44owRuBJEfVwXY MzELZn2ZZrkIf4/l1JauNvxIZd2lnFlnT67qWHT1w6m17GTeHmTAaoDMUWDdPs48LLsnekm2 4s3Cid+8D0CALyWSnSGquY7cAFVRUXX8Lir8qS7gMbYeVE4cIzgYteMqY4cl3tNxP4MyrqRp S/lBye1CjPX3BX6FOlDUVg7AJuHYHq1hShT0fUEMQn61n49T5yo6atDJZI7caN+qr5o1rhsV fgDcMicBfIJRzjaomxPYZ74pY1kVRKqmQPTY3b5OGZjJ8ZtF17T59vpXgrz7y1fXCO4uPw3r 6Ckyg6GE4EIQB5vDZqOZf/2lwGxsHERlfhcRUzNJtUPKkzg/JIzdX76lbkvOcAKIhjfwT3c2 gqLWE9Kqe7Iqo4z0d/ImaHZ89v1S7UiRhJXRjCJ46y3OC/W+nuY7bVBCOvYLyrAUG7U+bm5Y bQHxv7xB/QLgVJWvtcuCL1s168/u4PiqrIGnARpGHLHMwaiBr96eCbUw8hIsqBRy65Uok29Q QSX4NhcMriVP8WjHVIMfVJ3YuOG3PASuz/T8fVofBmmvHErpOKKARdIIh2BqC1BN78kYooqz NAotNMS9wHi2AEhNcyLj3wM+mnQfGYMVb4r6sMTDIPx0FV51FBFZZHABz77+9eEcJNUKEgsK TKIg6yEirhBnxKQf302HHnL/OxcmZVT5EwWlAFefwyEyojfm/s6/BxN6jBmHA1awyJO3/93J mU2ZVZ+Ir+D/mswicVON4x299qt2PFEFo3NJ1o1eKnxUUivUmHRIXwwIqCG5wYB6WNadTVH+ 7fexWr4OdovVN+kxTM8ACaJtNS6JeGdNCWb8CxkIyhBN5IhJyL/g6mlaHYPrV3qDd5ZaIjvu 7xx5OgpAUHkHXd4nkD4YrV2EZwbU1acPm1ESvx9+6VPEG3BEN13Nf5iNGjpEv5wyzf2HYNUx iCgyg+jl/hz6cpWkg0mOA==
  • Ironport-hdrordr: A9a23:1aEf0qEv5yL/HPrxpLqE3MeALOsnbusQ8zAXPiFKOHtom6Oj9/ xG8M576faWslgssRMb6LK90cC7KBu2n6KdirNhWItKMjOW3FdA77sO0aLShxPlEy36sshH1a lhdKB6TPn9F0Jzg8q/wCTQKadC/DBKysyVbC7loEtQcQ==
  • Ironport-phdr: A9a23:K4NiXxRMZ63Kyx5ToyEViQFT99psouWVAWYlg6HPa5pwe6iut67vI FbYra00ygOTBsOKs7kd1raempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yN s1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffQtFiCC5bL9uI xm6sAXcu8YLioZ+N6g9zQfErGFVcOpM32NoIlyTnxf45siu+ZNo7jpdtfE8+cNeSKv2Z6s3Q 6BWAzQgKGA1+dbktQLfQguV53sTSXsZnxxVCAXY9h76X5Pxsizntuph3SSRIMP7QawoVTmk8 qxmTgLjhiUaOD4j6GzYhcx+gqxYrhy8uRJw35XZb5uJOPdkZK7RYc8WSGhHU81MVyJBGIS8b 44XAuQaPOZYqZL9p1sPrRCjBQajHuXvyjBVjXLxxK060uIhERrG3AwhEdMDq2jbrM7vOKcKS +C1za/IwindYPNK3jf97pLEfQ48rvGRRL99d9faxkYzGQ3flFqQtZDlMC2P1uQLq2WX8ultW OCthmMjrwx8oyajy8gth4fJm44bxU7J+CZ6zYorK9O1Sk51bNCkHZZUty+UOJd7T8M8T211p Ss316ELtJimdyYJ0JQq3wPTZ+KEfoSS/x7vSfidLS1liH9reb+znRa//Ei4xuHiSsW51ExGo ylFn9XWq3wByR/e5tKHR/dj+EqqxCyB2BrJ6u5eJEA5jarbJIAlwr43jpcTr0XDHijymErok K+ZaEUl9faz6+j9frrmvYWQN5duigH/NKQhhtKwAfg/MggIRWSU5/mz1KD78U34RrVFkOE2n 7HEvJzEJskXvLO1DxJL3oo59hqyATar3M4YkHQHNF5FfQiIj4ntO1HAOvD4CvK/jky1kDdqw fDGJb3hApTDL3XYjLjhZqxx61ZGyAoyy9BQ+4xbCq0GIPL1QEP+qsHXDgIhPwyy2OnoEM992 Z8GWWKTHq+ZN7vfvUKQ6uI1P+aMfJMVuCr6K/U9+/HuimY5lUYBcqmtwJsYc2u1Hu9mIkWce XrjmM0NEWYMvgokTezlkkeOUTBJZyX6Y6Vp7TYiTYmiEI3rR4a3gbXH0j3oMIdRYzV/C1aXE XagSIyCVL9YcSOUOc9gjRQPTv65UY4n3hyyswm8xrZ6eLmHshYEvI7ugYAmr9bYkgs/oGQc5 6W11miMSzoxhWYUX3ot27g5p0Vhy1CF2Kw+gvpCFNUV6ekaGhwiO8v6yOp3Q8v3RhqHZs2AH U+nRM6mAC4ZRcl328UPZU1wB9KkyB3PwnniGKcbwoSCH4d86afAxz70Lsd5xWzB0fw4jl89Q spQHWa9wLZl9g7YCpLOlQOUm7v5Pb8E0nv1/XyYhXGLoFkeUAN0VvDdWmsDY0LNsdnjzl3DS LujFbk2PxAHwtXEMrFLbNbkkVJAAvrvJbwyekqXnGG9TVaNz7KIN8/xfnkFmT7aEA4CmhwS+ nCPMU4/AD2gqiTQFm4mE1WneE7q/eRkzRHzBkYp0wGHaVFg3Lup61YUg/KbUfYawrMDvm8ot Tx1GF+329+eBcCHokJte6BVYNV151kityqRrg17JZyhMIhpnRgGaQVxtE7y0BMxB4ld0IAro H4s0AtuOPeAyloSElHQlZv0O7DRNizz5EX2Mf6QgwiElo/NpOFStaddyR2rpgyiG0s8/m8y1 tBU1yDZ/ZDWFE8JVoq3VE8r9h98rrWcYy8n5oqS22c/VMv8+jLExd8tA/Mojxi6eNIKerqFE hTyEtIyDNPoMPYrnVOkchUCeu1e6eRnWqHuP+vDw6OtMOt6yXi/jGJc4IFi+kmXsTJmS+jD0 ooCxbeV0hbNBFKexB+x98vwn45DfzQbGGGynDPlCIBmbap3ZY8XCG2qLqVb3/1GjoX2Ez5d/ V+nXBYd3dOxPAGVdxr71BFR0kIepTqmnzG5xnp6iWNhoq2a1S3Ii+PsEXhPcndKQnJijEjEK pPyl8obWkOlcw8v0hap+A72yrNaq6J2M2TICR4SL26vdjskC/Du8OffK8dUjfFg+T1aSuG9f UyXRvbmrh0W3jmiV2pSyTYndi2775Dwnhh0kmWYfxMR5DLSfcB9wwua5cSJHKQBmGNfHm8h0 meRWwXvWrvhtc+ZnJrCrO2kAmeoV5kINDLu0ZvFryyjo2tjHRy4mfm33NzhCwkzlyHhhLwIH W3FqgjxZo7z2uG0K+ViKwNxBVnn68tlMopl1JMqhZcb1GQdgNOY8WdNwgKReZ1LnLnzanYAX 2tB2t/T+wjkx2VoNTSR3YP/XXiBxc0natWnKDBzuGp1/4VBD6Ga66ZBlC1+rw+jrA7fVvN6m y8U1fok7HNJy/FMogcmyT+RR6wDBUQNdzK5jAyGtprtyccfLHbqa7W701By2MysHK3X6B8JQ 273I98nDWdx9pktaQicliSqsMe9I4eWNZVJ7Xj221/BieNRNZ48xOIQhCxsNH76uzsox/Nzm xVq2dvSUJGvE2x25+r5BxdZMmawfMYP4nT2ir4YmM+K3oepF5EnGzMRXZKuQ+j6WD4VsP3mM U6JHlhe4j+DHqHDGAaE9Ep8h2zOFJSmK3yGKWJfxs4kXAOcIkdSnAcSGjg2g9Y1Gxury8rob Epig1JZrgei+l0Vk7gubkKhFDqC7A6zIi85Up2eMAZb4klZ6kHZPNbfpuN/EidE/4Gw+QyAL mvIAmYARWoNW0GCGxXiJuz3v4mGqrHCQLPlcb2TPObry6QWTfqDyJOx35Ez+j+NMp7KJXx+F 7gg3VIFW3llGsPfkjFJSioNliuLYdTIwXX0siBxsM279+zmHQz14o7aQaJTN85v+g+eirzFL /SRgi10NTFekJ4A2DWbrdpXlE5XkCxoezS3RP4YsjXRSavLhqJNJwAabCd+KMZZ4rl61RILI dTajNj4yrl+yPM5Fh0WMD6p0tHsbssMLWanMVrBD0veL7WKKwrAxMTvaL+9Q7ld361E8ge9s jGBHwr/LyyOwnP3Agu3P7gG30T5dFRO/ZuweRF3BS3/QcL6P1elZcRvg2R+yPVxj3fOfwb03 hB3aAVVtLyW5i5EhfM5FmBcvCMNxQishSee6+TEJ4cbqr1gGWJsjeNc63kmzL0T4S1ZFqUdc M76pcUou0unlOKC1j1hFhdCt2QT7L8=
  • Ironport-sdr: 5jqxYjdYdv85cbJIceqm9TGYdJHrAKJa0ZK+20gfSw32CoLvJs0tEfSrIBgyMcJ2F3kAWayJ+F sjHNZGE4XMrfbL7IthXPzP3N+Sw/tpEjRaapPHG44ztlH9rif1xDo6P5j9fRABhN+ulvg6+ivZ KHIaqEmOkd/v0hck3V4mN2sxpUxKxd32vPrD6fHI2QrpYFsjB/suVgT4++JTqleIOyne7B9nkP WVLUMP3yMse/i1YSKJfNm3nNowGjkoGp9dh6vRLbOWEHDPLGL8ge2YRp3ezq9Exe6qwj0KJXkW UkEoUdHqWaLO0FpciVunwVvi

Hi everyone,

Is there any way to make a "Definition" as opaque as a proof ended with "Qed"? My use case is I want to specialize a lemma and define
Definition foo := lem (* a lot of paramters *).
I want to omit its type, which is long. So I cannot start a "Proof." in a normal way.

Thanks,
Qinshi



Archive powered by MHonArc 2.6.19+.

Top of Page