Issue 777 [Re: [Agda] Semigroup.Carrier in 2.3.2]
Andreas Abel
andreas.abel at ifi.lmu.de
Mon Dec 31 09:35:53 CET 2012
Your example below works under Agda 2.3.2 if we bring H into scope with
{H = H}:
powerToPositive {H = H} x e e>0 = pow e e e>0
where
open Semigroup {{...}}
pow : Nat -> (e : Nat) -> e > 0 -> Carrier
However, this should not be necessary, I filed this as bug 777.
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/
More information about the Agda
mailing list