Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- data bool : Set where
- tt : bool
- ff : bool
- data ℕ : Set where
- zero : ℕ
- succ : ℕ → ℕ
- _+_ : ℕ → ℕ → ℕ
- zero + n = n
- succ m + n = succ (m + n)
- _<_ : ℕ → ℕ → bool
- m < zero = ff
- zero < succ n = tt
- succ m < succ n = m < n
- data _≡_ {A : Set} (x : A) : A → Set where
- refl : x ≡ x
- widen : ∀ m n p → (m < n) ≡ tt → (m < (n + p)) ≡ tt
- widen m zero p ()
- widen zero (succ n) p refl = refl
- widen (succ m) (succ n) p e = widen m n p e
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement