[Agda] darcs patch: Nat.Properties: add ∀ m n → m ≤ m ⊔ n

[Nils Anders Danielsson]

On 2009-11-26 17:47, Jean-Philippe Bernardy wrote:
> I seem to remember that this sort of theorem is available in a
> "Lattice" record somewhere in the std. lib.

No, there is no general code connecting, say, semilattices and partial
orders.

> I also remember that is was very cumbersome to extract it for
> convenient use.

I have seen in the past that people have had trouble extracting fields
from deeply nested records, even though the fields have been exported
from the top-level record module using open public. I think the main
problem is that it is hard to know which definitions are exported by a
module, so we are planning to add a feature which lists these
definitions:

  http://code.google.com/p/agda/issues/detail?id=207

--
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.