Skip to content

Instantly share code, notes, and snippets.

@juxtin

juxtin/LearnYouAn.agda

Created June 5, 2015 08:01
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save juxtin/2a9602c2193cc0a3dbbb to your computer and use it in GitHub Desktop.
Save juxtin/2a9602c2193cc0a3dbbb to your computer and use it in GitHub Desktop.
Download ZIP
Raw
LearnYouAn.agda
module LearnYouAn where
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
_+_ : ℕ → ℕ → ℕ
zero + zero = zero
zero + n = n
(suc n) + n′ = suc (n + n′)
data _even : ℕ → Set where
ZERO : zero even
STEP : ∀ x → x even → suc (suc x) even
proof₁ : suc (suc (suc (suc zero))) even
proof₁ = STEP (suc (suc zero)) (STEP zero ZERO)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment