Skip to content

Instantly share code, notes, and snippets.

@tomprince
Created April 6, 2011 14:33
Show Gist options
  • Save tomprince/905745 to your computer and use it in GitHub Desktop.
Save tomprince/905745 to your computer and use it in GitHub Desktop.
diff --git a/src/categories/cat.v b/src/categories/cat.v
index 6a5ef1e..65d38e7 100644
--- a/src/categories/cat.v
+++ b/src/categories/cat.v
@@ -11,12 +11,7 @@ Record Object := object
; Category_inst: Category obj }.
Implicit Arguments object [[Arrows_inst] [Equiv_inst] [CatId_inst] [CatComp_inst] [Category_inst]].
-Existing Instance Arrows_inst.
-Existing Instance Equiv_inst.
-Existing Instance CatId_inst.
-Existing Instance CatComp_inst.
-Existing Instance Category_inst.
- (* Todo: Ask mattam for [Existing Instance foo bar bas.] *)
+Existing Instances Arrows_inst Equiv_inst CatId_inst CatComp_inst Category_inst.
(* The above would be much more elegantly written as
@@ -30,8 +25,7 @@ Record Arrow (x y: Object): Type := arrow
; Functor_inst: Functor map_obj _ }.
Implicit Arguments arrow [[x] [y]].
-Existing Instance Fmap_inst.
-Existing Instance Functor_inst.
+Existing Instances Fmap_inst Functor_inst.
Instance: Arrows Object := Arrow.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment