[Agda] strict total order on characters

[Ramana Kumar]

As promised, here is a patch for a strict total order on strings (attached).
I'm not 100% sure it is producing something of the right type, so take a look.

On Mon, Nov 21, 2011 at 2:39 PM, Ramana Kumar <rk436 at cam.ac.uk> wrote:
> 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: stringsto.patch
Type: text/x-patch
Size: 15141 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20111121/1e6e8ee2/stringsto.bin