The Coq mailing list

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

Dear Coq users

for guiding  automation heuristics I sometimes need to classify terms. For 
this I am missing an ltac function has_var, similar to has_evar. Is there a 
way to implement this in ltac?

Also I wonder if there is a good way to check if a term is a literal, in the 
sense that it consists entirely of constructors, e.g. a literal number or 
boolean value or more complex term, but without vars, evars, matches or 
function applications. On a simplified term I guess checking not has_var and 
not has_evar would work.

Another useful thing would be an ltac function, which evaluates some sort of 
complexity measure of a term. I have some idea how this could be done, but 
before I try it, I wanted to ask if someone has something ready I could use.

Thanks and best regards,

Michael