coq-club AT inria.fr
Subject: The Coq mailing list
List archive
[Coq-Club] Ltac2: how to use ltac2 constr variables in calls to ltac 2 notations?
Chronological Thread
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Ltac2: how to use ltac2 constr variables in calls to ltac 2 notations?
- Date: Thu, 25 Jul 2019 12:35:11 +0000
- Accept-language: de-DE, en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga04.intel.com
- Dlp-product: dlpe-windows
- Dlp-reaction: no-action
- Dlp-version: 11.0.600.7
- Ironport-phdr: 9a23:fPn2cBICpa7CKnA2qtmcpTZWNBhigK39O0sv0rFitYgeLvXxwZ3uMQTl6Ol3ixeRBMOHsqgC27Cd7viocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmSSxbalxIRmoogncttUaipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3QqBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4qx2ThLjlSUJOCMj8GzPisJ+kr9VoA6vqRJ8wo7bfI6aOeFkca/Bed4XX3ZNUtpPWyFHH4iyb5EPD+0EPetAoYXzulwOogWxBQmwHuPvzSdIimfr1qM90uQuDQHG0xY+ENIKvnjfsdL4NKITUe+pzKnH1yvMb/dM1Tfm74jHbB8hoe2WXbJ3acrc0kgvFwXZjlqOrYzpJS+a1uMIs2WC6edrSOyhi2kiqw5rozivwN8hiojPhoIJ1F/E8T91z5srKtC+VUV1YsakHYNNuyyeKYd6WMMvTmFytCs61LEKo4O3cDYWxJg/2hLSavKKf5KG7x/tTuqdPzl1iXZ/dL6ihBu+7FCsxvD9W8SwylpGsCpIn9bWunwTzRDe6syKR/1g9Um7wzmPzRrc6uRcLEA0i6XbL5khz6Y1lpocq0vPAiD7lF/3jK+QakUr5Oyo5/77bbXho5+QL450igfgPaQygsGzHOA1PhYUU2Wb+emwzr3u8VPjTLlXkPE6jrHVsJXAKsQaoq65DRVV0oEm6xunCjem0cgXnXkdI11bfBKLlZPpO1bQL/D3Efe/mVOskC9wyvDHOL3hHovCLnzZnLj9erZ97lZQyBAvwtBH+5JUFrYBLervVU/2rdzUFwM2Mwipw+n8E9h9zYMfWWeXAqCDKq/SsFmI5vguI+aWfoMVtiz9eLAZ4Kukhngg3FQZYKOB3J0NaXn+EO4saxGSZmOpidMcG08LuBA/RarkkgvRfyRUYiP4ZKUx6S0hD5riRaLCTYCkjbjLlHO+H5ZWb21CTEuLHHj0bYKcc/YKdC+WZMRml2pXBvCaV4Y92ET250fBwL19I7+Mo3xKhdfYzNFwotbru1Q3/D1wAd6a1jjUHWBygm4MATQx2fIm+BEv+hK4yaF9xsdgO5lT6vdOC1hoMJHVl7A8CtbuVwaHddCMGg7/HoeWRAopR9d0+OcgJl5nEoz73BHFwyeuRbQSku7TCQ==
Dear Coq Users,
I wanted to write a simple tactic in Ltac2 to cbn just a given part of the goal, but I don’t understand how I can pass on a ltac2 variable to a call to a ltac2 notation. My example:
Require Import Ltac2.Ltac2.
(* Basic change syntax works *)
Ltac2 change4 () := change (2+2) with 4.
Goal 2+2=4. change4 (). Abort.
(* Error Unbound value term *)
Ltac2 change_nop (term:constr) := change $term with $term.
I tried quite a few things, but I don’t get around this error.
In the end I would like to do this:
Ltac2 cbn_flags_def := { (* beta: expand the application of an unfolded functions by substitution *) Std.rBeta := true; (* delta: expand transparent global definitions *) Std.rDelta := true; (* Note: iota in tactics like cbv is a shorthand for match, fix and cofix *) (* iota-match: simplify matches by choosing a pattern *) Std.rMatch := true; (* iota-fix: simplify fixpoint expressions by expanding one level *) Std.rFix := true; (* iota-cofix: simplify fixpoint expressions by expanding one level *) Std.rCofix := true; (* zeta: expand let expressions by substitution *) Std.rZeta := true;
Std.rConst := [] }.
Ltac2 change_cbn (term:constr) := change $term with ltac2:(Std.eval_cbn cbn_flags_def term).
Thanks & best regards,
Michael Intel Deutschland GmbH |
- [Coq-Club] Ltac2: how to use ltac2 constr variables in calls to ltac 2 notations?, Soegtrop, Michael, 07/25/2019
- Re: [Coq-Club] Ltac2: how to use ltac2 constr variables in calls to ltac 2 notations?, Pierre-Marie Pédrot, 07/25/2019
- RE: [Coq-Club] Ltac2: how to use ltac2 constr variables in calls to ltac 2 notations?, Soegtrop, Michael, 07/26/2019
- Re: [Coq-Club] Ltac2: how to use ltac2 constr variables in calls to ltac 2 notations?, Pierre-Marie Pédrot, 07/25/2019
Archive powered by MHonArc 2.6.18.