[Agda] Nat arithmetic properties

[Sergei Meshveliani]

On Thu, 2016-09-22 at 21:54 +0300, Roman wrote:
> Sergei, you seem to compute with records a lot, so I wonder: what will
> happen if you try to type check your development with the
> --no-eta-equality flag enabled? Or at least some part of it, if you
> actually use eta-rules somewhere.
> https://github.com/agda/agda/blob/14b9fbb11264a136f6b1e92373ee4a9149d006e4/CHANGELOG#L299
> 

Thank you for help.
I am trying this as

  agda --no-eta-equality $agdaLibOpt +RTS ... -RTS  TypeCheckAll.agda 
 
(without understanding its meaning, so far).
Some modules do type-check and others do not.
Is it possible to apply  no-eta-equality  to a separately selected
module, or separate record?

Thanks,

------
Sergei