The Coq mailing list

[Beta Ziliani <bziliani AT famaf.unc.edu.ar>]

What we do in Mtac is to use the typeclass mechanism to do the trick:

Class runner A  (f : Mtac A) := { eval : A }.
Arguments runner {A} _.
Arguments Build_runner {A} _ _.
Arguments eval {A} _ {_}.

Hint Extern 20 (runner ?f) => (exact (Build_runner f ltac:(rrun f)))  : typeclass_instances.

Hope it helps.
Beta

```

​

On Wed, Jun 1, 2016 at 5:15 AM, Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Gregory,

 

it is not an elegant solution, and maybe not a solution at all for your real case, but what I do in such situations is this:

 

Definition foon (ls : nat) : nat := 0.

Definition foob (ls : bool) : nat := 0.

Definition foonl (ls : list nat) : nat := 0.

Definition foobl (ls : list bool) : nat := 0.

 

Open Scope list_scope.

 

Ltac try_something :=

 lazymatch goal with

  | |- nat => exact 0

  | |- bool => exact true

  | |- list ?t => let value := fresh "value" in assert(t) as value by try_something; exact (value :: nil)

  end.

 

Notation "'it'" := ltac:(try_something) (at level 0).

 

Definition barn : nat := foon ( it ).

Definition barb : nat := foob ( it ).

Definition barnl : nat := foonl ( it ).

Definition barbl : nat := foobl ( it ).

 

This way at least the number of terms you need to specify is not the product of the number of base types and the number of parameterized types, but their sum.

 

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, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928