Skip to content

Instantly share code, notes, and snippets.

@hatashiro

hatashiro/s_k_lt_k_proof.idr

Last active May 2, 2017 06:08
Show Gist options
  • Save hatashiro/699b4947694961a78a49836196f87e09 to your computer and use it in GitHub Desktop.
Save hatashiro/699b4947694961a78a49836196f87e09 to your computer and use it in GitHub Desktop.
Download ZIP
A proof of '∀ k ∈ Z: 1 + k > k' in Idris
Raw
s_k_lt_k_proof.idr
module Main
%hide (>)
data (>) : (a : Nat) -> (b : Nat) -> Type where
ZeroCase : 1 + a > 0
OtherCase : a > b -> 1 + a > 1 + b
s_k_lt_k_proof : {k : Nat} -> 1 + k > k
s_k_lt_k_proof {k=Z} = ZeroCase
s_k_lt_k_proof {k=S _} = OtherCase s_k_lt_k_proof
@hatashiro
Copy link
Author

hatashiro commented May 2, 2017 •
edited
Loading

Reference (actually quite the same code): https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Nat.idr

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment