[Agda] Transitive-on

[Ramana Kumar]

On Thu, Nov 17, 2011 at 2:30 PM, Nils Anders Danielsson <nad at chalmers.se> wrote:
> On 2011-11-17 14:29, Ramana Kumar wrote:
>>
>> Char<-isTransitive : Transitive (_N<_ on Data.Char.toNat)
>
> The following code works:
>
>  Char<-isTransitive {i = i} {j = j} {k = k} =
>    Transitive-on (λ {i j k} → N<-trans {i = i} {j = j} {k = k})
>                  {i = i} {j = j} {k = k}
>
> But also the following:
>
>  Char<-isTransitive = N<-trans

Ah interesting... it seems like the useless-looking definition of
Transitive-on really was useless...

>
> --
> /NAD
>
>