roboguy13/Equal.v

Created January 27, 2018 09:43

Star (0) You must be signed in to star a gist
Fork (0) You must be signed in to fork a gist

Learn more about clone URLs
Clone this repository at <script src="https://gist.github.com/roboguy13/5917665321226f762e2c653a049bae8f.js"></script>
Save roboguy13/5917665321226f762e2c653a049bae8f to your computer and use it in GitHub Desktop.

Download ZIP

Raw

Equal.v

 Inductive Eq : Type -> Type :=
   | MkEq : forall a, (a -> a -> bool) -> Eq a.
 Definition my_equal {e b c : Type} {t : Type -> Type} (dict : Eq e) (f : forall a, t a -> e) (x : t b) (y : t c) : bool.
   destruct dict as [T eq].
   exact (eq (f b x) (f c y)).
 Defined.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment