The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

the "lia" tactic is like "omega" and can deal with min/max.

On 07/02/2014 04:34 PM, Jonathan wrote:
> Is there a version of omega that includes min and max?  I know one could
> write a tactic that uses lt_dec to case-analyze away all mins and maxes
> - I am just wondering if this has already been done - or, perhaps even
> something more efficient that wouldn't bother to explore the entire space.
>
> -- Jonathan