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

[Jean-Philippe Bernardy]

I seem to remember that this sort of theorem is available in a
"Lattice" record somewhere in
the std. lib. I also remember that is was very cumbersome to extract
it for convenient use.

Is that correct? Is there a canonical way to use lattice (and maybe
other) structures?

Thanks,
JP.

On Thu, Nov 26, 2009 at 3:45 PM, Nicolas Pouillard
<dedibox.feydakins.org at gmail.com> wrote:
> I agree to release my library patches under the library's licence
>
> Thu Nov 26 15:36:32 CET 2009  Nicolas Pouillard <nicolas.pouillard at gmail.com>
>  * Nat.Properties: add ∀ m n → m ≤ m ⊔ n
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>