[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
More information about the Agda
mailing list