Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
agda.agda
data : Set where
zero :
suc : (n : ℕ)
{-# BUILTIN NATURAL ℕ #-}
infixl 6 _+_
_+_ : (n m : ℕ)
n + zero = n
n + suc m = suc (n + m)
infixl 7 _*_
_*_ : (n m : ℕ)
n * zero = zero
n * suc m = n * m + n
infix 4 _≡_
data _≡_ {A : Set} (x : A) : A Set where
≡intro : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}
≡elim : {A : Set} {x y : A} {α : A Set} α x x ≡ y α y
≡elim αx x≡y rewrite x≡y = αx
suc-func : (n m : ℕ) n ≡ m suc n ≡ suc m
suc-func n m n≡m rewrite n≡m = ≡intro
suc-inj : (n m : ℕ) suc n ≡ suc m n ≡ m
suc-inj n .n ≡intro = ≡intro
lem-0+ : (n : ℕ) (zero + n ≡ n)
lem-0+ zero = ≡intro
lem-0+ (suc n) rewrite lem-0+ n = ≡intro
tut5-3c : (n : ℕ) (n * 1 ≡ n)
tut5-3c n = lem-0+ n
infix 4 _<_
data _<_ (n m : ℕ) : Set where
pf< : (k : ℕ) n + k ≡ m n < m
data Ordered (n m : ℕ) : Set where
less : n < m Ordered n m
same : n ≡ m Ordered n m
more : m < n Ordered n m
order : (n m : ℕ) Ordered n m
order zero zero = same ≡intro
order zero (suc m) = less (pf< (suc m) (suc-func (zero + m) m (lem-0+ m)))
order (suc n) zero = more (pf< (suc n) (tut5-3c (suc n)))
order (suc n) (suc m) with order n m
... | less (pf< k ≡intro) = less (pf< k {! !})
... | same n≡m = {! !}
... | more m<n = {! !}
data isEven : Set where
zero : isEven zero
2+ : {x} isEven x isEven (suc (suc x))
data isOdd : Set where
1+ : {x} isEven x isOdd (suc x)
data Partition (n : ℕ) : Set where
even : isEven n Partition n
odd : isOdd n Partition n
even-or-odd : (n : ℕ) Partition n
even-or-odd zero = even zero
even-or-odd (suc zero) = odd (1+ zero)
even-or-odd (suc (suc n)) with even-or-odd n
... | even x = even (2+ x)
... | odd (1+ x) = odd (1+ (2+ x))
safesub : {n m} m < n
safesub (pf< k x) = k
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.