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: Re: [Coq-Club] normalize all closed terms of a given type
- Date: Wed, 14 Oct 2020 22:41:19 -0700
- Authentication-results: mail3-smtp-sop.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-f178.google.com
- Ironport-phdr: 9a23:Lnji6hN9SCcr07+ba7ol6mtUPXoX/o7sNwtQ0KIMzox0IvXzrarrMEGX3/hxlliBBdydt6sbzbSM+PG/EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe/bL9oLRi6swrdu80UjIB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgzoFOTEk6mHaksN/jKxZrxyhqRJxwJPabp+JO/dlZKzRYckXSHBdUspNVSFMBJ63YYsVD+oGOOZVt5XwqEAOrRu/HgmsBP3gyjxVjXLq2601yeIhHhzb1wEnBd0Bq3TUrNTuNKcST++1z7PEwi/Fb/xM3zfy9ZLEchEgofGQUrJ9asXRyUw1GAPEilWcs5DqPzSQ1ukUtWWQ8uVvW/61hWE9twFxviagxt0qioTRgo8YykzI+DtnzIg7K9C2SE92bcC4HJdNty+UN4t4Tt0sTmx0pCs3xKAKtIOlcCUI1Jkq2x/SZfOIfoWI/x/uVeCcKip2inJifbKwnRey8U64x+LgUcm0ylBKoTRBktnIrHwCyQHc6tWBR/Bg/UmhwS6C2x7P5uxAO0w5lqrWJ4Q8zrMxl5cfq1nPEy31lUjwkaSYbF8r+vKy5OTierjmpoGTN4tzigzmN6QhgM2/AeAhPggPW2iX5P2w1LP+8UD7Q7hGlPI2kq7esJDVIcQUuLS1DBNS0oYm8xq/DjGm38oEnXQfMl5JZBaKg5LqNlzOOvz0EPayjlW2nDt2xf3LPaXtApDXIXjClLfhc6x960lZyAcr199Q/JJUCrAaIPLzREDxt8bUAQU/MwOuxeboFc9x1oIfWWKTDa+UK6zSsVqS6eIuJ+mAfpMauDH4K/Q9/f7hkWc5mUMBfamuxZYYdHe4Hu1/L0qFZXrsn8wOHHwRvgs+SezqkEeNXSRSZ3a0RaI85ys0BJioDYfZFciRh+mK2z7+FZlLbCgSAVeVVHzsao+sWvEWaSvULNU3wRIeUr30YoUh1AquuQyy4rxuKOacriQStZP41NV2oeTVnBc+sz11E8u13GSETmUylWQNEWxllJtjqFBwnw/QmZNzhOZVQIQKtqF5FzwiPJuZ9NRUTtX7WwbPZNCMEQ/0TdCvADV3RdU0kYZXPhRNXu66hxWG5BKERr8Yk7vRWs4x+6PYmnn1foNzkimWkqYmiFYiT41EMmj03vcjpTiWPJbAlgCir4jvbb4VhXef+2KKzG7It0ZdAlZ9
Sorry, I was not clear. I want to only strongly normalize closed subterms of the type and leave the rest unchanged.
On Wed, Oct 14, 2020 at 6:54 PM Jason Gross <jasongross9 AT gmail.com> wrote:
Sorry, that only does goal, but doing the context isn't much differentOn Wed, Oct 14, 2020, 20:53 Jason Gross <jasongross9 AT gmail.com> wrote:Here is a slow tactic to do this:Ltac norm T :=repeat match goal with| [ |- context [?e] ] => let e' := eval vm_compute in (e : T) in progress change e with e'end.You may want a different typing check if you don't want coercion insertion or only want to check up to syntactic typing rather than unification.On Wed, Oct 14, 2020, 20:20 Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote: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.... ?-- Abhishekhttp://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
- 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, Beta Ziliani, 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, 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
Archive powered by MHonArc 2.6.19+.