Skip to content

Instantly share code, notes, and snippets.

@andrewthad

andrewthad/diet_set_gadt.hs

Created May 18, 2018 18:53
Show Gist options
  • Save andrewthad/8536c07c9b0ac00e2f7ce9f9e2094fc4 to your computer and use it in GitHub Desktop.
Save andrewthad/8536c07c9b0ac00e2f7ce9f9e2094fc4 to your computer and use it in GitHub Desktop.
Download ZIP
Diet Set GADT
Raw
diet_set_gadt.hs
data Nat = Z | S Nat
data TwoGt :: Nat -> Nat -> Type
TwoGtNil :: Gt ('S ('S n)) 'Z
TwoGtStep :: Gt n m -> Gt (S n) (S m)
data Diet :: Nat -> Type where
DietNil :: Diet 'Z
DietCons :: forall n m. Gte n m -> TwoGt m p -> Diet p -> Diet n
data DietX = forall n. DietX (Diet n)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment