The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  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

  The motivation is as follows, on the following pattern:

context[ match nth _lst _i _d with ... end ]

  if _lst is a concrete variable, then I want to run a tactic which considers the cases:

  length _lst <= i \/

  i = length_lst - 1 \/

  i = ... \/

  i = 2 \/

  i = 1 \/

  i = 0

  Now, the issue is: I only want this to happen when _lst is a "concrete variable."

  If all I know is that _lst is a "list nat", then I don't want to run this tactic.

  Thus, my question: how can I test if a variable has a "concerete" value? (a negative of "it's not known to be possible" though highly unlikely, would be useful too)

Thanks!