The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hello --

I'm wondering if anyone has a trick to get tactics-in-terms to fire later? Here's a somewhat contrived example:

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

Ltac try_something :=

  lazymatch goal with

  | |- nat => exact 0

  | |- bool => exact true

  end.

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

Definition bar : nat := foo (it :: nil).

In the last line, we know that the type of 'it' should be [nat] since [foo] takes an argument of type [list nat]. However, when the Ltac actually fires, the goal is a unification variable and therefore neither of branches of the [lazymatch] matches.

Any hackish tricks to get this to work? Possibly something involving 'Program' or canonical structures?

-- 

gregory malecha

gmalecha.github.io