coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] check whether a variable is in the context of an evar
- Date: Thu, 21 Sep 2023 13:49:22 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f42.google.com
- Ironport-data: A9a23:splBeqkSeHpm1yfFBmlGLjno5gz1I0RdPkR7XQ2eYbSJt1+Wr1Gzt xIZXGDXa/nba2fxftFzPYyz9h9Uu5SBn4NrGVZu+ypgFVtH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayajl8B56r8ks156yj4mpA5TTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN1hHRtsM6Qfo99bDGIf9 aQxL2xTdxKM0rfeLLKTEoGAh+wmJcjveZwa4zRukWufAvEhTpTOBa7N4Le03h9q3pEITauYP pBJL2Y1BPjDS0Un1lM/AZg+nfyoi3q5ejtRrl7TpKsr7EDcyQVw1P7mN9+9ltmiHJ8KxBnG9 jqfl4j/KioFFObHwxyMyVaT3bfoggfmeakXHZTto5aGh3XWnAT/EiY+Xlyi5PK9l0SWQMNaM 0VS+yw0rKF0+lbDczXmdxixoXrBoRtFHtQMSas17waCzqeS6AGcboQZcgN8hBUdnJdebVQXO pWhxrsF3BQ+6+XHemHX7bqOszK5NA4cKGJIN2dOThII75On6Ms/hw7GBIQrWqOkrMzHKRepy RCzrQ86m+oyi+wP3P6F5lzpuW+niaXIaQ8X3T/peFyZwDl3X6OfXLzw22Pnta5BCK27Umi+u GM1npnCzeIWUrCIui+/YMQMO7CL4fy6HiXWqgNtFcN59hCG2X2qTaZP6h5QeWZrNcclf2fyQ Unx4Al+2r5aDEGIX4RWPb2jKp0N5rfyMPjYTdboV8pqTrktUR6Y7QdsSFW13WuwoHMzkKo6B 4iXQfysAVkeF65j6ji8HMUZ7pMG2QE8wnH1V7ng7hH6z4ebWmGZeY0FPHSKcOo9yqGO+yfR0 tRHMvq12wdta/L/bgbX4LwsAwgzd1ZjPq/PqutTauKnCShlEjt4C/bunJUQS7Y8lKFRzur17 nWxX3FD82XGhFrFF1SuSmtiY7bRT5pAvSoFHSgzD22JhVknQ6iStZk6SbVmXIMa5NRCzOF1R cYrY8+vIOpCYRWZ9iU/bavSlp1DdhOqjz2gJyCOOWM1Q7N8dQ7w6/vhchXlriUVPBHqt8Fk+ 7yE/SHYSKolWA5NIpv3avWu7lXpplkburt4cHXpK+lpWnfH0dZVOQnuqP4oMucwKRnn7RmL5 Ta8WBs3i7HEnN4ozYPvm6uBkbaML8J/OUhrR0/g8re8MHjhzFqJmINvfr6BQmHAaTnS5q6nW ORyysP8Ot0hmHJhkdJ1M5Rv/JIEy+rfnZ1o5SU6IyyTdHWuMK1qHVee18oWtqFt+K5QiTHrZ m2xoOtlKZe7E+K7Nm5JPwc0TPWx5ddNkBno0PkFCkHb5ih2wbm5bXtvLyS80BJ6Er8kH74mk MEAudEX4TORkhAFEMiLpQEK+nWuLk4vabQGtJYbMtWyigMU1UxzO83AKy7p4aOgb8dHHVkqL wS12ovDpeV47WjTf0UjEUPi2bJmuq0PnxRR3Xk+KE+siPOcotMKhDhq7iUQYiFO6xd2w8ZfG zNMCRVuBKOs+zxIupByb1q0EVscOCzDq13D9VQZsUb4EWy6XXPpB08gM7+v+Es5zTptTgJD9 uvF9Fe/ACfYR+Cv7C4cQkU/lufCS+Z2/Qj8mMyKOcSJMp05QDj9iJ+Vems6hEr7MPw1mXH4i 7FmzMRoZY3/EBwgkakxJo2Z9LYXER66fT0IBbkr+a4SBmjTdQ2jwTXEeQj7ZspJIOeM6kOiT dBnIsVUTRmlySKStXYhCLURJ6Nv1uscjDbYlmgH+UZd21dektZojH4U3i33hWtuXNA31Mhhc MXecDWNFmHWjnxR84MIQA+oJULgCeTopiWltAx2zAnNP50GueBoN0o119NYel2LZRB/8Uv8U BzrPsfrIi8L9Wiot4TpG6RHQQ6zLLsfkQhOHB+b67xzUD8EDSsCW875ZLUq08S68Ib9g+hKq Ik=
- Ironport-hdrordr: A9a23:kEiUH68PUOkQQF12ml5uk+DVI+orL9Y04lQ7vn2ZKCYlFfBw8v rFoB11726WtN98YhEdcLO7WZVoI0msl6KdiLN5VdyftWLdyQ6Vxe9ZnO/fKv7bdxEWNNQx6U 6tScdD4RTLY2RHsQ==
- Ironport-phdr: A9a23:2zyrHhENrarCg2AGTrvdV51Gf6lGhN3EVzX9CrIZgr5DOp6u447ld BSGo6k30hmQDduQsqsZw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PSbglSmTawYrJ/I BqroQnMtsQdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3U bJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5 LptRRT1iikIKiQ5/XnYhcJwgqxVow+vqQJjzIPPeo6ZKOBzc7nBcd8GR2dMWNtaWSxbAoO7a osCF/YMMv1Yr4n8vFsOrQWxBQqxD+7zzD9HnHn20rAn2OkmCw7JxwwgH9MVsHTUstr1N70eX vqzzKbSyzXMcula2Tb86IjUfRAsuv6MXbdqfsrQzUkjDR/KjlKVqYH8OT6ey+sCvXSB4eV6S eKvl3Aoqxt3ojW32MoiipfEi58ax17L6Ch13og4KcO7RUNnb9OqEIVcui6eOoZ0X88vQXxlt SY6xLAEupO2fjQGxIo5yxPcaPGKfY6F6Q/tWuaWJDd3nnNleLSnihmu9kig0Ov8Wdew0FZOt CZKjMTDtm0L2hfO6caHUuNw8lm91TuLzQze6eFJLVopmabFKJMt2LE9moQVvE/eBCH5gl/2g 7WTdkg8+uin9eDnYrL+q5+ZLYB0iwX+Pr0gm8y6HOg0KwYOUmeF9eim273j+kr5QLpOjvIoi KXWrJfaJcEDqq64BQ9azJoj5g6hAzu61NkUh3oKIVJfdB6akYTkOEvCLf/mAfunhlSjijZrx /TIPr37BZXNK2DOn636crZ96k5c0wozws5c555OEL4BJuj8Wknsu9DCDx85MhC0w+n8BdVy0 4MRQ2OPAquDPKzOtl+I4/ojI++Xa4ANojbyN+Al5+LyjX8+gVIRYLGl3YELZ3CgAvRmP0KZb GLwjdcGCGcGpxYxTOj3iFKZSjNTfHazX6ck5j4hEo6mDIHDRpqsgLObxiu7EIdWNSh6DQWHF m6tfIGZUb9YYyWLZ8RljzYsVL67SoZn2wv45yHgzL8yB+DU+zYYuJGr/d584eGbwRg49T1vD 8melWiLRmd42GIJWzAe06V2oEg7wVCGh/sry8dEHMBesqsaGjwxMoTRmrQS47HaXwvAeo3MU 1O6WpC8Bjp3SNstwtgIakI7GtO4jxmF0TD5S6QNmemtA5o5urnZw2C3P9x0nn/M1Kg6j1QlB MJJPGuqwK9+6wf7CIvAkkHfnKGvJuwHxCCYzG6Y1iKVuV1AFgt5UKHLR3caM0LcrdXi5k7BC baoALIrdApA1cGqJa5Da9mvhlJDF7/4INqLRWW3li+rAAqQgLOBaI2/Y2IGwCDUE1QJiSgW9 HeCcBc7X2Kv/ziYAztpGlbiJUjr9IGSsVudSUk5h0GPZkxljf+u/wINwOabQLUV164FvyEor 3N1Gky81pTYEYjIoQ0pZ6habd4nhTUPnWvEqwxwOIChJKF+lxYfdQpwpUbnyxRwDM1Jj8Erq HogyAc6J7if1RtNcDaR3Ja4PbOySCG69RqvarXW11KY2dCf/KtJ6fUkpH3suQioEgwp9HAmm 9hZ3n2A54nbWRIIWMGUMA5//Bx7qrfGJyglstmMhDs8bO/t6G+Eh4h6YYltggytdNpeLq6eQ Qr7EslAQtOrNPRvgV+iKBQNIOFV8qcwecKgbfqPnqCxb4MC1Hqri3pK5Idl3weC7S15H6TB1 ZYE2PGV3U2OUT76gBGgs9z4sY9BbDAWWGG4zGK3YewZLr03ZosNBWq0doe+zNV/nJ7gWDhR8 lelCxUH2dOmURWXZl35mwZX0A5ExB7v0Tv9xDtynTYzq6OZ1yGb2OXuei0MPWtTTXVjh1PhS WStp+gTR1PgLw0glR//oF3/27AevqN0aW/aXUZPeSHyaWBkSKq58LSYMYZD75YhsCMfV+rZA xjSQ7T9ogAa3iClFm1Xwjx9djC2tb32mhV7jCSWK3M7oHfCeM52zAvS/5SGHa8XjmdAHXMoz 2WNTlGnWrvhtc2ZjZLCrvyzWyq6W5tffDOqhYKMuS2n5HF7VBi2nvS9gNriQkAx1S720cUvV D2d9k6tJNm2kf3gYaQ7JBoNZhe08cdxF4Bgn5FlgZgR3SJfnZCJ5T8dlmy1N9xH2KX4ZX5LR DgRwteT7hK2vS8rZn+P2Y/9UW2Qh8V7YNzvKGoc2iMm781JTq6S5bpI2yp0vlWQogfYYPw7l TAYg6hLijZSk6QStQwhwz/ISLkYHUhDPSHv0R2O5tay6qRWeGmHfr251U44ltekRuLnwEkUS DPyfZEsGjV158N0PQfX0XH93YrjfcHZcdMZshDH2weFleVeL4g90+YbnScyc3yopmUrkqRo6 H4mlYH/poWMLH9hub60EgINfCOgfNsdo3nslfoMxZvQhtH3WM89RXNTG8G0BfOwTGBM6bK9b F3ISWNk7C/cQOu6f0fX6V86/SyRVcnzbTfPYiFel40qRQHBdhIBxlpIDXNqxthhUVryjM35L BUmvHZIuhih+0EKkqUxZ3ydGi/evFv6NWtyEcLCakIQtkYbuQ/UKZDMt7ojWXgHodvx6lTKc DXTZhwUXzhWAQrdVgylZv/2ooCelorQTuumc6mUOeTI+bEYDq3Yg8roi9Qu/i7QZJ/WYD8/X 7tiixAFBTcgSozYg2ldEXVJ0XiWPojA/lHkvXQmy6L3uOLiXAaljWeWI51VN9gnuxW/gKPZc vWVmD48MzFTkJUF2X7PzrEbml8UkSBnMTe3Q/wGsmbWQaTcl7UybVZTYj5vNMZO86M33xVcc c/dhNTv07dkj/kzQ15bXF3lk8utaIQEOWa4fF/AAU+KMvyBK1ipi4nvZrigTLRLkOhOnxi5u DLeDEq6ezrfzX/mUBegNewKhyaefVRftIy7bhdxGD3jQdbhOXjZeJd8iTw7x6Fxh2ufbzZNd 2ghNRoX/vvMt3A94L03AWFK43t7IPPRni+Y67OdMZMKqb5xBS8yketG4XM8wr8T7SdeRfUzl jGBy7wm61ygjOSLzSJqFRRUrTMezouBvUR5OajasJBGUHDIuhMM8Wq4BBEDpt8jAdrq8fM1q JCHhOfoJTFO/siBt9MbHNTRIdmbPWAJNBPoHHvLCVJAQ2Lxc27YgENZnbeZ8Xjf/f1Y4tD83 ZEJTLFcTlk8EPgXX19kENI1K5ByRjo4kLSfgabgAFKxqRDQQINRuZWVDpp64N3qITedyKZBP l4Gnem+IoMUOYn2nUdlbwsi9GwlM0XVVNFJ5CZma11tyHg=
- Ironport-sdr: 650c824f_2XVnuihKzXdbqQYHbCD3Es97leAEj2TLt0mUYPgct9OPyVL v8tmfL4GEey8rz74xy8ZJJ0oe1JIjqKmLbz9z/A==
Is there a way to check whether a variable is in the context of an evar?
In my use case, I am trying to instantiate the evar and if the variable is not in context of the evar, I need to first make it existentially quantified.
-- Abhishek
http://www.cs.cornell.edu/~aa755/- [Coq-Club] check whether a variable is in the context of an evar, Abhishek Anand, 09/21/2023
- Re: [Coq-Club] check whether a variable is in the context of an evar, Ike Mulder, 09/22/2023
Archive powered by MHonArc 2.6.19+.