[Agda] Re: strict total order on characters

[Ramana Kumar]

How would I add to the standard library, if the answer to question 2
below were 'yes'?

On Fri, Nov 18, 2011 at 11:53 AM, Ramana Kumar <rk436 at cam.ac.uk> wrote:
> I have three questions about the following snippet.
>
> -----8<-----
> open import Relation.Binary using () renaming (IsStrictTotalOrder to
> ISTO;StrictTotalOrder to STO)
> open import Data.Nat.Properties renaming (<-trans to N<-trans;
> strictTotalOrder to Nsto)
> import Data.Char
> import Relation.Binary.On as RelOn
>
> infix 4 _Char<_
> _Char<_ : Rel Data.Char.Char _
> _Char<_ = _N<_ on Data.Char.toNat
>
> Char<-StrictTotalOrder = record
>  { Carrier            = Data.Char.Char
>  ; _≈_                = _≡_ on Data.Char.toNat
>  ; _<_                = _Char<_
>  ; isStrictTotalOrder = RelOn.isStrictTotalOrder Data.Char.toNat
> (STO.isStrictTotalOrder Nsto)
>  }
> ------8<-----
>
> 1. (How) Can I show that (_≡_ on Data.Char.toNat) is the same as _≡_?
> Is there a hope of using the latter for the _≈_ field of the record?
>
> 2. Would code achieving the above not be appropriate for the standard
> library? And (probably using it) an ordering on strings too?
>
> 3. Do you have any comments whatsoever on how to improve the style and
> clarity (given that this was written by a novice)?
>
> (4. the second last line was yellow for a while, but now it seems to
> be loading fine... I think all I changed was the order in which I
> opened/imported stuff...)
>