# [Agda] Semigroup.Carrier in 2.3.2

Serge D. Mechveliani mechvel at botik.ru
Sun Dec 23 12:09:26 CET 2012

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