Skip to content

Instantly share code, notes, and snippets.

@LeifW

LeifW/type_in_thing.idr

Created February 26, 2015 21:42
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save LeifW/87296bfc3d1b9081d1c7 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save LeifW/87296bfc3d1b9081d1c7 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
type_in_thing.idr
data X : Type where
Y : Type -> X
getA : X -> Type
getA (Y x) = x
f : X -> (getA X)
--f (Y Int) = 10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment