The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/02/2014 10:37 AM, Robbert Krebbers wrote:
> the "lia" tactic is like "omega" and can deal with min/max.

Thanks for pointing that out, Robbert!

-- Jonathan

> 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