From 4e5aa4bcc6024aa7add9c1bf1c2ad9fd2a6a3685 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 11 Apr 2011 00:09:26 +0000 Subject: [PATCH] uncomment some code in ProgrammingLanguage.v --- src/ProgrammingLanguage.v | 20 +------------------- 1 file changed, 1 insertion(+), 19 deletions(-) diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v index 7ac2af7..e29903a 100644 --- a/src/ProgrammingLanguage.v +++ b/src/ProgrammingLanguage.v @@ -171,21 +171,7 @@ Section Programming_Language. Instance Types_assoc a b : Types_second a >>>> Types_first b <~~~> Types_first b >>>> Types_second a := { ni_iso := fun c => Types_assoc_iso a c b }. -(* - intros. unfold functor_comp. unfold fmor. - Opaque Types_assoc_iso. - simpl. - - eapply cndr_inert. - apply pl_eqv. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_prod; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. -*) -admit. + admit. Defined. Instance Types_cancelr : Types_first [] <~~~> functor_id _ := @@ -216,7 +202,6 @@ admit. ; pmon_assoc_rr := Types_assoc_rr ; pmon_assoc_ll := Types_assoc_ll }. -(* apply Build_Pentagon. intros; simpl. eapply cndr_inert. apply pl_eqv. @@ -254,9 +239,6 @@ admit. auto. eapply cndr_inert. apply pl_eqv. auto. auto. -*) -admit. -admit. intros; simpl; reflexivity. intros; simpl; reflexivity. admit. (* assoc central *) -- 1.7.10.4