Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- data _⊔_is_ : ℕ → ℕ → ℕ → Set where
- m≥⊔nism : {m n : ℕ}
- → n ≤ m
- ---------
- → m ⊔ n is m
- m≤⊔nisn : {m n : ℕ}
- → m ≤ n
- ---------
- → m ⊔ n is n
- data Total (m n : ℕ) : Set where
- forward : m ≤ n → Total m n
- flipped : n ≤ m → Total m n
- ≤total : (m n : ℕ) → Total m n
- ≤total zero n = forward z≤n
- ≤total (suc m) zero = flipped z≤n
- ≤total (suc m) (suc n) with ≤total m n
- ... | forward m≤n = forward (s≤s m≤n)
- ... | flipped n≤m = flipped (s≤s n≤m)
- _⊔_ : (m n : ℕ) → Σ[ p ∈ ℕ ] (m ⊔ n is p)
- m ⊔ n with ≤total m n
- ... | forward m≤n = ⟨ n , m≤⊔nisn m≤n ⟩
- ... | flipped n≤m = ⟨ m , m≥⊔nism n≤m ⟩
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement