Ssreflect Users Discussion List

[Bas Spitters <>]

Yesterday over lunch we had a similar discussion whether omega/lia would work for non-standard arithmetic.

In theory it should of course, it is just another model of PA/HA.
However, the backend may not be so flexible.

On Tue, May 6, 2014 at 8:05 PM, Laurent Thery <> wrote:

-------- Original Message --------

Subject:	Re: [ssreflect] omega and mathcomp
Date:	Tue, 06 May 2014 20:04:52 +0200
From:	Laurent Thery <>
To:	Maxime Dénès <>

On 05/06/2014 07:59 PM, Maxime Dénès wrote:
> I've always wondered (because I'm not using these things a lot), is 
> there any reason to prefer omega over romega?
>

The implementation is a matter of taste (reflexive or not) but from what 
I recall they don' t solve
exactly the same goals so you can' t replace blindly one by the other.