[Agda] trivial lemma of `with'

[Sergei Meshveliani]

On Tue, 2013-12-31 at 01:02 +0100, Andreas Abel wrote:
> The problem is that in the last case, "| no _", you have two different 
> proofs of y /= 0.  You probably intend that dRem is independent of the 
> proof of y/=0.  One way is to state that using irrelevance, then your 
> proof goes through:
> 
>    record Foo : Set (α ⊔ α=)
>      where
>      field  _≟_  : Decidable _≈_
>             dRem : (x y : C) → .(y≉0 : ¬ y ≈ 0#) → C
> 
>      eQuot : C → C → C
>      eQuot x y  with y ≟ 0#
>      ...      | yes _  = 0#
>      ...      | no y≉0 = dRem x y y≉0
> 
>      lemma : {x y : C} → (y≉0 : ¬ y ≈ 0#) → eQuot x y ≈ dRem x y y≉0
>      lemma {x} {y} y≉0 with y ≟ 0#
>      ...              | yes y=0 =  ⊥-elim (y≉0 y=0)
>      ...              | no  y≠0 =  refl
> 

!!
Thank you. This dot usage is new for me.

1. Is it explained in some manual?

2. For example,  Data.Nat.DivMod._divMod_  of  lib-0.7  has signature
 
   (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
   DivMod dividend divisor

Will there arise difficulties in proofs caused by that  ≢0  is not
dotted here?

3. In my real program, I have

   field eucNorm : EuclideanNorm
         divRem  : (x y : C) → (y≉0 : y ≉ 0#) → DivRem eucNorm x y y≉0 

Setting dot on the first "y≉0" causes an error report. So, I try this:

         divRem  : (x y : C) → .(y≉0 : y ≉ 0#) → DivRem eucNorm x y _


in a hope that the checker knows what to put for `_'.
Is this a regular solution?

Thanks,

------
Sergei