[Agda] Semigroup.Carrier in 2.3.2

[Serge D. Mechveliani]

Thank you very much.
I shall try, and see.
Agda looks good.

Regards,

------
Sergei

On Mon, Dec 31, 2012 at 08:17:14AM +0100, Andreas Abel wrote:
> Agda 2.3.2 has the new feature of sections (anonymous modules) you
> could make use of.  It allows you to write the type signatures
> without painful lets.
> 
> In your case:
> 
> module _ {c l : Level}{H : Semigroup c l} where
>   open Semigroup {{...}}
> 
> -- Power  x  to a positive degree  e.  The binary method.
>   powerToPositive : (x : Carrier) (e : ???) -> e > 0 -> Carrier
>   powerToPositive x e e>0 =  pow e e e>0
>      where
>      pow : (cnt : ???) (e : ???) -> e > 0 -> Carrier
>         -- cnt  is the counter used in termination proof
> 
> Instance search succeeds in this case, but if you are want to open
> Semigroup locally only anyway, you could also directly write
> 
>   open Semigroup H
> 
> which is both clearer for the reader and for Agda. ;-)
> 
> Cheers,
> Andreas
> 
> On 30.12.12 5:14 PM, Serge D. Mechveliani wrote:
> >On Tue, Dec 25, 2012 at 09:26:00AM +0100, Andreas Abel wrote:
> >>Instance search is experimental, so it is likely not all things work
> >>the same.
> >>
> >>Could you please attach a test case I can try directly without have
> >>to do imports, renaming etc.?
> >
> >
> >See the attachment to this letter:   Main.agda.zip.
> >
> >The first variant there works under  Agda-2.3.0.1
> >but not under                        Agda-2.3.2.
> >
> >The second variant is commented out,
> >it "fixes" the code for 2.3.2 by making the argument explicit.
> >
> >Which Agda version is more correct at this point?
> >
> >Regards,
> >
> >------
> >Sergei
> >
> >
> >>On 23.12.12 12:09 PM, Serge D. Mechveliani wrote:
> >>>People,
> >>>this program is accepted in by Agda-2.3.0.1
> >>>and rejected by                Agda-2.3.2 :
> >>>
> >>>---------------------------------------------------------------
> >>>powerToPositive : {c l : Level} -> {H : Semigroup c l} ->
> >>>             let C = Semigroup.Carrier H in  C -> (e : Nat) -> e > 0 -> C
> >>>--
> >>>-- Power  x  to a positive degree  e.  The binary method.
> >>>
> >>>powerToPositive x e e>0 =  pow e e e>0
> >>>      where
> >>>      open Semigroup {{...}}
> >>>      pow : Nat -> (e : Nat) -> e > 0 -> Carrier
> >>>         -- cnt  is the counter used in termination proof
> >>>
> >>>      pow 0         _             _  = x
> >>>      pow _         0             ()
> >>>      pow _         (suc 0)       _  = x
> >>>      pow (suc cnt) (suc (suc e)) _  =
> >>>                               (if even? e then  p * p  else (p * p) * x)
> >>>                               where
> >>>                               half = suc $ quot2 e
> >>>                               p    = pow cnt half $ positiveHalf? e
> >>>---------------------------------------------------------------
> >>>
> >[..]
> >
> 
> -- 
> Andreas Abel  <><      Du bist der geliebte Mensch.
> 
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
> 
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
>