[Agda] _divMod_
Andreas Abel
andreas.abel at ifi.lmu.de
Mon Sep 3 23:13:08 CEST 2012
Hello Serge,
On 03.09.12 8:02 PM, Serge D. Mechveliani wrote:
> 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
It seems that you forgot to rename _mod_ to mod2 in the last line.
> 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.
If you define mixfix operators like
_divMod_ : ...
_divMod_ = ...
then you can use them by filling terms for the underscores, like
m divMod n
or you use it prefix
_divMod_ m n
Only in prefix usage you can supply hidden arguments.
> (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?
The termination checker might complain, depending on your definition of
myDivMod...
> May be _divMod_ is better, this needs studying;
> and so far, I only try to apply _divMod_.
Cheers,
Andreas
--
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