Skip to content

Instantly share code, notes, and snippets.

@LeifW

LeifW/MyEq.idr

Created December 31, 2015 02:51
Show Gist options
  • Save LeifW/e54dfbd8654b9c800d1a to your computer and use it in GitHub Desktop.
Save LeifW/e54dfbd8654b9c800d1a to your computer and use it in GitHub Desktop.
Download ZIP
Nothing special about Idris's (=) type.
Raw
MyEq.idr
%default total
data MyEq : a -> a -> Type where
MyRefl : MyEq a a
myTrans : MyEq a b -> MyEq b c -> MyEq a c
myTrans MyRefl MyRefl = MyRefl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment