coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Doing eta-expansion in Ltac

From: Serguei Lenglet <serguei.lenglet AT univ-lorraine.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Doing eta-expansion in Ltac
Date: Tue, 30 Jul 2019 12:11:36 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=serguei.lenglet AT univ-lorraine.fr; spf=Pass smtp.mailfrom=serguei.lenglet AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f180.google.com
Ironport-phdr: 9a23:DOaQ2xLDvKj2gk5BttmcpTZWNBhigK39O0sv0rFitYgRL/XxwZ3uMQTl6Ol3ixeRBMOHsqgC2rGd6fiocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmSSxbal2IRi4ogndqNUaipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3QqBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4qx2ThLjlSUJOCMj8GzPhcN+jKxVrhG8qRJh34HZe5uaOOZkc67HYd8WWWhMU8BMXCJBGIO8aI4PAvIcM+lGtYn9qEYOogW/BQKxAu3g1DlIhnDy3aIkz+QqDAbL3Bc+ENIUv3TUscv6NKYIXeCx0qbIyzrDb/dI1jfh84XIbxYhofCSXb5pdcrRzlMvFxnfgVWRr4zqISmZ1uoXs2WC6edrSOGhi3Y/pg1vvjSiwt0gh4rJi44P1FzI6zt1zJwoKdC7VEJ2Z8OvHoFKuCGALYR2R9svQ2F2tyY+zb0LoZu7czILyJQj3hLfcv+Hf5WR7hLtSeqcIit0iGhqeLK4gBay/kygxfPmWsao11ZKqzJJktjKtn8Tyxze8taLRud580u72juC1xrf5v9aLUwqj6bXNp0szqIompoWq0vDHyv2mEvsjK+Rc0Up4vOo5Pr9YrXpu5+TKY50hhv6MqswnMy/DuA4PRYSX2WA9uS80afs/Uz9QLlQkvI2lazZvIjAJcsHvq65HxNV0oE75hmjCDemyc0UkmUDLFJYYx2KlJPpOlHLIPDgF/izmVWskDFxx/DHJLLtGJvNLmKQ2IvmKL168gtXzBc55dFZ/ZNdTL8bc9zpXUqkj9HCAQI0MkSQzuDoDNhhntcFVHiAH6KYdqfft1CM6/4HPu+NesoRvyznIvkj6rjglylqyhcmYaC10M5POziDFfN8LhDBOCe+spI6CW4P+zEGYqnqhVmFC2ABYn+zW+cl5Wh+Btv2VcHMQYeihLHH1yC+TMUPNzJ2T2uUGHKtTL2qHvIFaSacOMhky2VWWr2oSotn3har5lajl+hXa9HM8yhdjqrNkcBv7rSDxww09CIxC8OHyWiMSWwykHlaHzI=

Hello

I am trying to write a tactic to do some eta-expansion. I have written something like

match goal with
| [ H : ?P x = ?Q |- _ ] => match Q with
context E [x] => let f := (fun y => context E[y]) in
change (P x = f x) in H
end

but the function "fun y => context E[y]" is a meta-level (Ltac level) function and not a term level function. Is there a way to turn it into a term level function ?

With best regards

Sergueï

[Coq-Club] Doing eta-expansion in Ltac, Serguei Lenglet, 07/30/2019
- Re: [Coq-Club] Doing eta-expansion in Ltac, Tej Chajed, 07/30/2019