Skip to content

Instantly share code, notes, and snippets.

@zraffer

zraffer/idris-error-inductive.idr

Created November 30, 2014 19:46
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save zraffer/0de0f4b1133dc0902e04 to your computer and use it in GitHub Desktop.
Save zraffer/0de0f4b1133dc0902e04 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
idris-error-inductive.idr
mutual
data T1 : Type where
Mk1 : T1
Mk2 : T2 Mk1 -> T1
data T2 : T1 -> Type where
Mk0 : T2 Mk1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment