The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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