[Agda] strict total order on characters

[Ramana Kumar]

Oh what you wrote was already complete.
I have packaged it up as a patch and attached to this email.
I will try to get a strict total order on strings working next, hopefully...

On Mon, Nov 21, 2011 at 12:46 PM, Ramana Kumar <rk436 at cam.ac.uk> wrote:
> 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
>>
>>
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: charsto.patch
Type: text/x-patch
Size: 14839 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20111121/ea9043bf/charsto-0001.bin