Ssreflect Users Discussion List

[Benjamin Werner <>]

Hello Keiko,

From what i know:

- for now, omega is not really compatible with ssrnat. We can
hope for a streamlined version of omega which would, but
not immediately.

- One can write a small Ltac script to "translate" goals
from ssrnat to regular nat (replacing the operations, the boolean
operators, the equality and`inequality operators by their
respective counterparts.

I did write such a script quickly. It was a little slow but
could be useful. I'll try to find it in my files.

best,

Benjamin



Le 8 déc. 08 à 13:09, <> < 
> a écrit :

> Hello,
>
> If I decided to use ssrnat, then I have to give up the omega tactic?
>
> Best regards,
> Keiko