coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Discovering instances of a type class inside a Coq ml tactic
Date: Sat, 13 Jan 2018 19:36:50 -0600
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
Ironport-phdr: 9a23:JSMalRBpeXNP4ym48/cpUyQJP3N1i/DPJgcQr6AfoPdwSPryr8bcNUDSrc9gkEXOFd2Cra4c0qyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUmTaxe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJOT43/n/KhMJzgqJUrw6uqAF9zIHae4yVKOZyc7nBcd8GX2dNQMBcXDFBDIOmaIsPCvIMM+ler4nnplsBsRy+DhSyCuz10T9InX721rA93us/FwHGxg0gEM4JsHjOsNX6LrwSUfu0zKTTzDXDaelW2Tbn54TSfBAhu+iBULRtesTS0UkiDwfIg1qKpYD7MT6ZzOUAvmyB4+Z9S+6iiXYrpg5zrzS128shhZfFipgLxlzY7yl13og4KN2+RUVme9CrCoFQuDufN4ZuQsMtXWVouCEix70Ip5G7YDQKyIkhxx7DcfOLaY+I4gjsVOqJIDd4gmxqeK6nihu2/kWs0PPwW8eu3FtLqidJiMTAum4P2hDL78iIUPp9/kOv2TaV0ADT7/lJIU8umqrBNZEh2aU9lpQNvkTfAi/2hUP2jLOMeUk+/eio8evnbq38ppCAL490lh3+MqM2l8OjBuQ4KxECUHSf+eShz7Lu5lb5QbVPjv0uiKbVqpHaJcIBpq64GQBZyIgj6wzsRwuhhd8fhDwMKE9PUBOBlYngfV/Uc97iCvLqrlK2kTxsj8zPJabgSsHAKGLCm7CnYb9m8E90yQwpzNkZ6YgCWeJJG+76RkKk7I+QNRQ+KQHhm7+2WuU47ZsXXCe0OoHcNarTtVGS4ed2f7uCaZMJpTDhIr4i/fG81SZly29YRrGg2N4sUF79Bu5veh3LYHz2g95HH31Y5lNjHtyvs0WLVHtoX1j3X6844WhnWoyrEZveQJykxrub03XjEw==

On Sat, Jan 13, 2018 at 05:36:35PM +0000, Kenneth Roe wrote:
> 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?

I use Typeclasses.instances <glob_ref> (or Typeclasses.all_instances) in
order to fetch TC instances for a given global class name (or the entire
TC database).

There is also Typeclasses.is_class to check if a global_reference is a
class or not.

Best,
--
Enrico Tassi

[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