[Agda] ⊓ in Nat

Sergei Meshveliani mechvel at botik.ru
Sat Apr 22 21:52:27 CEST 2017


On Sat, 2017-04-22 at 20:35 +0200, Andreas Abel wrote:
> Dear Sergei,
> 
> well, there is
> 
> m⊓n≤m : ∀ m n → m ⊓ n ≤ m
> m⊓n≤m zero    _       = z≤n
> m⊓n≤m (suc m) zero    = z≤n
> m⊓n≤m (suc m) (suc n) = s≤s $ m⊓n≤m m n
> 
> and there is commutativity of the minium.
> [..]

> Together, you get what you need. 


Indeed, I missed this name of  m⊓n≤m.

Thank you.

------
Sergei



More information about the Agda mailing list