coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proper morphisms for family of functions

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Proper morphisms for family of functions
Date: Tue, 5 Jan 2016 21:28:41 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=None smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-ob0-f177.google.com
Ironport-phdr: 9a23:RbPuCBOwakNP3+ohXM4l6mtUPXoX/o7sNwtQ0KIMzox0KP7+rarrMEGX3/hxlliBBdydsKIazbKO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStCU15z//tvx0qOQSj0AvCC6b7J2IUf+hiTqne5Sv7FfLL0swADCuHpCdrce72ppIVWOg0S0vZ/or9YwuxhX7vkm7otLVbjwV6U+V71RSjo8YE4v48i+ixDPTA7H1HIYU3sf2k5WEQHB7Q/zdpz0r233uvcri3rSBtH/Ub1hAWfq1KxsUhK90Co=

On Jan 5, 2016, at 21:14 , Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

2) Fields of typeclasses are NOT automatically added to the database used for typeclass resolution. You need to mark that explicitly by replacing ":" with ":>".
For example, rewrite works in your `bar` after you change your `MO2` as follows:

Class MO2 (mop: (A->A) -> (A->A) -> A -> A) :=
mop_proper :> Proper (((=) ==> (=)) ==> ((=) ==> (=)) ==> (=) ==> (=)) (mop).

Thanks! I just tried this and it did not work even though I can see mop_proper instance via 'Print Instances Proper’.

I am using Coq 8.4.

Sincerely,
Vadim Zaliva

CMU ECE PhD candidate

Mobile: +1(510)220-1060

Skype: vzaliva

Re: [Coq-Club] Proper morphisms for family of functions, Gregory Malecha, 01/01/2016
- Re: [Coq-Club] Proper morphisms for family of functions, Vadim Zaliva, 01/01/2016
- <Possible follow-up(s)>
- Re: [Coq-Club] Proper morphisms for family of functions, Vadim Zaliva, 01/06/2016
  - Re: [Coq-Club] Proper morphisms for family of functions, Abhishek Anand, 01/06/2016
    - Re: [Coq-Club] Proper morphisms for family of functions, Vadim Zaliva, 01/06/2016
      - Re: [Coq-Club] Proper morphisms for family of functions, Abhishek Anand, 01/06/2016
        
        Re: [Coq-Club] Proper morphisms for family of functions, Vadim Zaliva, 01/06/2016
        
        Re: [Coq-Club] Proper morphisms for family of functions, Abhishek Anand, 01/08/2016