[Agda] Transitive-on

[Nils Anders Danielsson]

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

-- 
/NAD