[Agda] equality on Integer

[Nils Anders Danielsson]

On 2012-08-10 14:13, Serge D. Mechveliani wrote:
> and trying to find:  what is this  _Б┴║_  (\dashTriple)
> (a kind of an identity relation).
>
> First, what is its intended meaning?

In this case: propositional equality of integers.

> Further, I am trying to trace this import of _Б┴║_ (\dashTriple).

If you want to see the definition of a symbol you can jump to it (M-. in
Emacs if the file has been loaded successfully).

> Digression on the export syntax: --------------------
> Haskell  has the syntax of    module Foo (T(), f1, f2)  where ...
>
> which means that _only_ the items  T(), f1, f2  are exported
> (and the instances for T()).
> If  Agda  had,  and the libraries used such an export construct,
> would not it be easier to read and find the import trace?
> Because in this case one can look only at the export part and skip the
> rest module source. The Haskell library uses this approach, and this
> helps a lot to understand the source.
> -----------------------------------------------------

If you want to see what symbols a module exports you can use the "Module
contents" command (C-c C-o).

> Probably, this `open' still exports the relation domain  \dashTriple from
> Relation.Binary.Core  -- even though its submodule is called Dummy.
> Is this so?

Yes, open M public reexports the module M:

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Modules

-- 
/NAD