[Agda] Semigroup.Carrier in 2.3.2

[Andreas Abel]

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/