The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/02/2014 01:18 PM, Xavier Leroy wrote:
> Alternatively, "zify; omega" can also deal with min, max, and a number
> of other things that "omega" alone doesn't handle.  If you run "zify"
> alone, you'll see how it replaces min and max by equivalent logical
> specifications that "omega" understands.
>
> - Xavier Leroy

Thanks, Xavier.  I didn't know zify existed.

-- Jonathan

> On 02/07/14 16:37, Robbert Krebbers wrote:
> > 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