The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 10/07/2013 02:48, t x a écrit :

>    With apologies for a vague-ish question (the word "concrete" must
> certainly have a technical definition): I want to see if a variable has
> a concrete value.
>
> example non-concrete:
> lst: list nat
>
> example concrete:
> lst: 1 :: 2 :: 3 :: nil

Ltac is_concrete_list l :=
  match l with
  | cons _ ?l => is_concrete_list l
  | nil => true
  | _ => false
  end.

Then you just have to test the boolean and behave accordingly.

Note that matching is purely syntactic, so, depending on what you want 
to achieve, you might need Coq to perform a bit of computations 
beforehand, e.g.

Ltac is_concrete_list l :=
  let l := eval hnf in l in
  match l with
  | cons _ ?l => is_concrete_list l
  | nil => true
  | _ => false
  end.

Best regards,

Guillaume