Skip to content

Instantly share code, notes, and snippets.

@JakobBruenker
Created November 19, 2020 11:19
Show Gist options
  • Save JakobBruenker/38251269a93cdd1f4979b771e613f4e6 to your computer and use it in GitHub Desktop.
Save JakobBruenker/38251269a93cdd1f4979b771e613f4e6 to your computer and use it in GitHub Desktop.
{-# LANGUAGE TypeFamilies, UndecidableInstances, KindSignatures, DataKinds, TypeOperators, GADTs, RankNTypes, PolyKinds #-}
import Data.Kind
import Data.Type.Equality
data Nat = Z | S Nat
data SNat :: Nat -> Type where
SZ :: SNat Z
SS :: SNat n -> SNat (S n)
type family Plus n m where
Plus Z m = m
Plus (S n) m = S (Plus n m)
plus_Z :: SNat n -> Plus n Z :~: n
plus_Z SZ = Refl
plus_Z (SS n) | Refl <- plus_Z n = Refl
plus_succ :: SNat n -> SNat m -> S (Plus n m) :~: Plus n (S m)
plus_succ SZ _ = Refl
plus_succ (SS n) m | Refl <- plus_succ n m = Refl
plus_comm :: SNat n -> SNat m -> Plus n m :~: Plus m n
plus_comm SZ m | Refl <- plus_Z m = Refl
plus_comm (SS n) m | Refl <- plus_comm n m
, Refl <- plus_succ m n
= Refl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment