[Agda] strict total order on characters

[Ramana Kumar]

Thanks a lot for the reply!
I would be happy for you to finish and add what you wrote below to the
standard library.
Alternatively, I can try to put something together and then send a
darcs patch, which might be good practice for me.
Up to you; let me know.

On Mon, Nov 21, 2011 at 12:41 PM, Nils Anders Danielsson
<nad at chalmers.se> wrote:
> On 2011-11-18 12:53, Ramana Kumar wrote:
>>
>> 1. (How) Can I show that (_≡_ on Data.Char.toNat) is the same as _≡_?
>
> This depends on what you mean by "the same". You can't prove that they
> are propositionally equal.
>
>> 2. Would code achieving the above not be appropriate for the standard
>> library? And (probably using it) an ordering on strings too?
>
> Yes. Yes.
>
>> 3. Do you have any comments whatsoever on how to improve the style and
>> clarity (given that this was written by a novice)?
>
> I might write something like this:
>
>  module Data.Char where
>
>  …
>
>  import Data.Nat as Nat
>  import Data.Nat.Properties as NatProp
>  open import Function
>  open import Relation.Binary
>  import Relation.Binary.On as On
>
>  …
>
>  -- A strict total ordering of characters.
>
>  strictTotalOrder : StrictTotalOrder _ _ _
>  strictTotalOrder = record
>     { _<_                = Nat._<_ on toNat
>     ; isStrictTotalOrder =
>         On.isStrictTotalOrder toNat
>           (StrictTotalOrder.isStrictTotalOrder
>              NatProp.strictTotalOrder)
>     }
>
> --
> /NAD
>
>