coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Discovering instances of a type class inside a Coq ml tactic

From: Kenneth Roe <kendroe AT hotmail.com>
To: Coq-Club <coq-club AT inria.fr>
Subject: [Coq-Club] Discovering instances of a type class inside a Coq ml tactic
Date: Sat, 13 Jan 2018 17:36:35 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kendroe AT hotmail.com; spf=Pass smtp.mailfrom=kendroe AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM02-CY1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:KDgJCxDAVSSHj4R18cUlUyQJP3N1i/DPJgcQr6AfoPdwSPv5ocbcNUDSrc9gkEXOFd2Cra4c0qyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUmTaxe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNyA3/nzLisJ+j6xUvB2uqgdlzILIfI2YLuZycr/Acd4cWGFPXtxRVytEAo6kaoUAEewBPeBGoInhp1sFsAewBQ6yC+jyzTJIhWH53asn3OQ7FgHJwhctH9IJsHTIqdX6LqYSUeSvwKbUyjXDaupb1DHg44bLahAsuf6BUa5qfcfV10UjDQzIgk+UpID7OT6ey/4DvHKB7+V6UOKik24npB91ojio3soikpXEiIUJxlza7Cl03oQ6KcChRE58etGrDoFctyaHN4tqWcwiRHxouCAnxbEcoZ67Zi8KyIg5yBHDd/yHco+I4hT5WOaWPDd4mHZleLW4hxax60Sv1ur8Vsys3FZLqCpKjMXMu2gC2hDP8MSKTuVx8l2u1DqV0w3f9PlIIUUumqraL54hzKQwlp0WsUnbHS/5hkP2g7KMdkUj5Oel8OTnYrL6pp+ZLYB0iwX+Pr4ylcy4BOQ0KhIOUHSD+eSgyL3j+lX0T6lNjv0vi6XWrJTaJdkAqaOiGA9U0oMj6w6lADu80dQYm2MHLFNfdx6dgYjpIQKGHPetJvCmxn+ojT0jk/vBJ/jqBojHBnnFirboO7hnvR1y0g02mPNS4ZRZFrFJGvX+EhvyudrUFBg0Gwyz3+PuCdE73YQbDzHcSpSFOb/f5AfbrtkkJPOBMddM6WTNbsM97vurtkcX3FoUfK2nx5wSMSvqHvN6JkyYZTznhdJTSD5W7Dp7d/TjjRi5aRAWf2y7Bvlu5jYnDYunCcHIQYX/2OXcjhf+JYVfYyV9Mn7JEXrscNnbCdElTXrIZ+RQy3kDX7XnTJI93xazsgO806BgMuff5iwfs9TkycRx4OrQ0xo18G4tAg==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Suppose, I have the following type classes:

Class ACprop {T} (f : T -> T -> T) : Prop :=

{

acProp : forall a b c, (f a (f b c))=f (f a b) c /\ f a b=f b a

}

within my code, I have many instances that look like this:

Instance acPlus : ACprop plus.

Inside my ml-tactic, I would like to either 1) collect up all of the instances of ACprop or 2) given a term such as "plus", determine whether "plus" is an instance of ACprop. This call can be called from inside the "Proofview.goal.enter" construct. What is the best approach?

- Ken

[Coq-Club] Discovering instances of a type class inside a Coq ml tactic, Kenneth Roe, 01/13/2018
- Re: [Coq-Club] Discovering instances of a type class inside a Coq ml tactic, Enrico Tassi, 01/15/2018
  - Re: [Coq-Club] Discovering instances of a type class inside a Coq ml tactic, Matthieu Sozeau, 01/15/2018