[Agda] _divMod_
Serge D. Mechveliani
mechvel at botik.ru
Mon Sep 3 20:02:49 CEST 2012
People,
I have a question on Nat.DivMod of Standard library
(of Agda-2.3.0.1, lib-0.6):
need to study how to use _divMod_.
Nat.DivMod has an example of such usage: the function _mod_.
I copy the _mod_ definition from Nat.DivMod to my module Main.agda
with changing the identifiers as
_mod_ -> mod2, \?= -> eq?, \nequiv 0 -> p
(see the _mod_ code in Nat/DivMod.agda):
----------------
mod2 : (dividend divisor : Nat) {p : False (divisor eq? 0)} -> Fin divisor
mod2 m n {p} with _divMod_ m n {p}
.(toNat r + q * n) mod n | result q r = r
----------------
-- for this email, I write Nat for \bn, eq? for \?= ,
in order to avoid problems with math symbols in email.
The report is: "Missing with-clauses for function mod2".
(1) Nat.DivMod.agda is compiled, and Main.agda is not:
can you explain this effect?
I thought, probably, the last line applies a _view_, similar as the
User Guide explains in Section `3.1 Views'.
At the moment, I do not understand `views'. But I look into the Guide
example of Parity and `parity' in this section, and just try to mimic
it. I change the implementation to
--------------
mod2 m n {p} with _divMod_ m n {p}
mod2 .(toNat r + q * n) n | result q r = r
--------------
(the second line has two arguments before `|', instead of the three
arguments in Nat/DivMod).
I do not know of _what_ this computes, but at least it is compiled.
I wonder what all this story may be about.
(2) Why it is chosen a name _divMod_ having two underscores?
It is not declared as infix.
(3) My beginner's attempt of divMod might be like this:
record MyDivMod (dividend divisor : Б└∙) : Set
where
field
quot : Б└∙
rem : Fin divisor
proof : (dividend Б┴║ quot * divisor + (toБ└∙ rem))
myDivMod : (n : Б└∙) -> (m : Б└∙) -> False (m Б┴÷ 0) -> MyDivMod n m
myDivMod n m p = ...
Will this approach work?
May be _divMod_ is better, this needs studying;
and so far, I only try to apply _divMod_.
Thank you in advance for explanation,
------
Sergei
More information about the Agda
mailing list