coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] normalize all closed terms of a given type

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] normalize all closed terms of a given type
Date: Wed, 14 Oct 2020 18:19:23 -0700
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-il1-f180.google.com
Ironport-phdr: 9a23:z73niBPzEIoIu36ZiFsl6mtUPXoX/o7sNwtQ0KIMzox0IvX/rarrMEGX3/hxlliBBdydt6sbzbSM+Pq9EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe/bL9oLRi6swrdutcWjIB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgzoFOTEk6mHaksN/gqJVrhyiuhJx3ZLbbZqPO/ZiZK7QZ88WSXZDU8tXSidPApm8b4wKD+cZIetXtIn9p1oVrRu+GwasB/7kxyNOhnDs2601zvkqHAbc0wM7H9IOsW/UrNXrO6cRS+y61q/Iwi/Fb/xLwzv96YnIcgwuofyXUrJwdNDeyUgrFw/fklqQronlMiqT2+8QvGeV8/BuWvizi247tQ5xuD6vy98yh4fJmI8Y11/J+ypkzYorK9C0Vk12bMKqHZVQqS2XOI97T8E/T2xqpSs3yr0ItJy4cSUI1Jgr2QDTZv+EfoWG5B/oSeifITB9hH1/ebK/gQ6//lSnyu3mUMm7zlJKri5fntbSq38Nyhre4dWERPtl5kqtxyqD2gTJ5uxHIU04j7fXJp8gz7Iqi5YesljPEynrk0vslqCWbF8r+u2w5uTnfLrmopicOpdxig7kM6QuntWzAeU8MgQTRmSb9/mw2b7/8UHjT7VKifo2kqbdsJ/EP8gUuqm5AwpN3oYi7RawESum3cwGkXUbKF9JYhGKgojzN13TIf31DO2zj0mvnTt33/zGO6fuApTJLnjNirfherN95lZGxwUozdBf5olUCrEfL/LwQEP+rtrYAQU/MwOp2ernCdR91p8RWW+UDa+ZNbndsV6M5u41P+aMY4oVtC7nK/c5//7ukWM5mVgFcKa12psXcWm0EehiI0WEenXhmcwBEGcPvgomVuPmklyCUThJZ3azRa0w/D87CJj1RbvEE4uqmfmK2DqxVsldYXkDAVSRG1/pcZ+FUrECcnTBDNVml2ktX7igUI8s1lmHsgb8x/IzJ+DU+zYYuJGl3d584eGVlBAu+hR7Cs2c1yeGSGQizTBAfCM/wK0q+R818VyEy6Ut26UER+wW3OtAV0IBDbCZ1/ZzUomgVQfIf9PPQ1GjEI3/XGMBC+kpytpLWH5TXtWviheZgXivCr4R0r2PXdk6q/KEmXf2IMl5xjDN06xz1wB3EPsKDnWvg+tEzyaWAofIl0uDkKPzLPYT2SfM8CGIym/c5Uw=

Is there a tactic to strongly normalize all closed terms of a given type in the Coq goal and context?

Is there a way to write such a tactic in Ltac/Ltac2/Mtac2.... ?

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] normalize all closed terms of a given type, Abhishek Anand, 10/15/2020
- Re: [Coq-Club] normalize all closed terms of a given type, Jason Gross, 10/15/2020
  - Re: [Coq-Club] normalize all closed terms of a given type, Jason Gross, 10/15/2020
    - Re: [Coq-Club] normalize all closed terms of a given type, Abhishek Anand, 10/15/2020
      - Re: [Coq-Club] normalize all closed terms of a given type, Fabian Kunze, 10/15/2020
        
        Re: [Coq-Club] normalize all closed terms of a given type, Beta Ziliani, 10/15/2020
        
        Re: [Coq-Club] normalize all closed terms of a given type, Abhishek Anand, 10/15/2020
        
        Re: [Coq-Club] normalize all closed terms of a given type, Jason Gross, 10/16/2020
        Re: [Coq-Club] normalize all closed terms of a given type, Jason Gross, 10/16/2020