[Agda] _<=_ and _<_

Sergei Meshveliani mechvel at botik.ru
Wed Sep 25 17:29:21 CEST 2013


On Wed, 2013-09-25 at 17:04 +0400, Sergei Meshveliani wrote:
> Please, how to prove          x < y → x ≤ y
> 
> in the general setting under  lib-0.7  ?
> [..]

Probably, it is by  DecTotalOrder  + Relation.Binary.StrictToNonStrict,
that is the definition for _≤_ to be taken from StrictToNonStrict.

I'll try and see.

------
Sergei




More information about the Agda mailing list