Skip to content

Instantly share code, notes, and snippets.

@hnsl

hnsl/gist:2ec70a739cadb2af9583

Created August 9, 2015 21:11
Show Gist options
  • Save hnsl/2ec70a739cadb2af9583 to your computer and use it in GitHub Desktop.
Save hnsl/2ec70a739cadb2af9583 to your computer and use it in GitHub Desktop.
Download ZIP
hello world with proofs
Raw
gistfile1.txt
module Main
total
minusS : (n : Nat) -> (m : Nat) -> LTE m n -> Nat
minusS n m x = n - m
total
decNat : Nat -> Nat
decNat k with (isLTE 1 k)
decNat k | (Yes prf) = minusS k 1 prf
decNat k | (No contra) = 0
main : IO ()
main = putStrLn $ "Hello world " ++ (show . decNat $ 4)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment