[Agda] Semigroup.Carrier in 2.3.2

[Andreas Abel]

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.?

Cheers,
Andreas

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
> ---------------------------------------------------------------
>
> Here I use the denotation (for this letter):
>   \bn --> Nat,
>   \.  --> *,
>   \~~ --> ~~
>   \_1 --> _1
>   quot2 : Nat -> Nat   the integer part of quotient by 2,
>   positiveHalf?        a certain user function.
>
> Agda-2.3.2  reports
>
> -------------------------------
> ...
> No variable of type
> Semigroup
> (_c_226 .Carrier ._~~_ ._*_ .refl .sym .trans .assoc .*-cong x e e>0
>   e)
> (_l_227 .Carrier ._~~_ ._*_ .refl .sym .trans .assoc .*-cong x e e>0
>   e)
> was found in scope.
> when checking that the expression Carrier has type
> Set
> (_225 .Carrier ._~~_ ._*_ .refl .sym .trans .assoc .*-cong x e e>0
>   e_1)
> -------------------------------
>
> Which is more correct, Agda-2.3.0.1 or Agda-2.3.2 ?
> How to fix?
>
> Also there is a question about  Standard library :
> does it remain  lib-0.6 ?
>
> My program  Main.agda  imports  lib-0.6,  and I use the same sources
> of  lib-0.6 as under  Agda-2.3.0.1яя.
> Now, when   Agda-2.3.2  compiles  Main.agda,
> it type-checks and compiles all the modules in  lib-0.6  which are
> are needed for the import in  Main.agda,
> right?
>
> Thanks,
>
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
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/