Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Ltac2: how to use ltac2 constr variables in calls to ltac 2 notations?

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
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928




Archive powered by MHonArc 2.6.18.

Top of Page