Skip to content

Instantly share code, notes, and snippets.

@UnkindPartition

UnkindPartition/proof.hs

Created July 31, 2015 11:11
Show Gist options
  • Save UnkindPartition/0bc7970696ea155d5358 to your computer and use it in GitHub Desktop.
Save UnkindPartition/0bc7970696ea155d5358 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
proof.hs
{-# LANGUAGE GADTs, DataKinds, TypeOperators #-}
{-# OPTIONS_GHC -Wall #-}
data Nat = Z | S Nat
data m <= n where
Le_z :: (n <= n)
Le_s :: (m <= n) -> (m <= S n)
type (m < n) = (S m <= n)
theorem :: (m < S n) -> (m <= n)
theorem prf =
case prf of
Le_z -> Le_z
Le_s prf1 -> lemma_1 prf1
lemma_1 :: (S m <= n) -> (m <= n)
lemma_1 prf =
case prf of
Le_z -> Le_s Le_z
Le_s prf1 -> Le_s $ lemma_1 prf1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment