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: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Discovering instances of a type class inside a Coq ml tactic
Date: Mon, 15 Jan 2018 10:12:11 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f45.google.com
Ironport-phdr: 9a23:HCB9LBTwgefgdnliBLK0oRZOgtpsv+yvbD5Q0YIujvd0So/mwa68bR2N2/xhgRfzUJnB7Loc0qyK6/mmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfa5+IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/27ZisNyjKxVrhGvqQFhzYHIe4yaLuZyc7nHcN8GWWZMXMBcXDFBDIOmaIsPCvIMM+FCoInhu1sOrRq+ChexBOjy1zFIgX730rMg3OQ8DArL2wkgEMgSsHTIttr1MbwfUeWvw6nU0TXMdfZW1S366IjSfRAsuPeBVq9zf8rJ0UQiFQzIgk+NpYD7Pz6ZzOcAv3aB4+dvVe+ijXMspRtrrTi13Mgsj5HEhoILxVDA8iV02IM1Kse5SE5/eNKlHp5Quz2DO4t4Tc4vQ3tkuCk9yr0Btp67eDYFxI47yB7YbvyLa4mI4hT9W+aNOTp1hn1odKiiixqs8UWs0O7xWteu3FtFridJitzMuWoM1xzX5MiHUPx9/kK51DaKzQ/T9v1EIUA1laXFNp4t2KUwlp0SsEvdBCD2hV77jKCTdko+++io7/7rbanhpp+ZL4N0kB3xMrwymsyjBuQ1KhQBX2+C+eilyLLj+VD5T65Rg/0tkqjZtYjaKt4Bqq64BQ9VyIcj5AylAzeoytRL1UUAeVlCYVeMi5XjE1DIOvHxS/ml0Hq2lzI+4vnaIr3gD4iFFX/Rnb78NeJ44lJAwQ8byNlD+5tRTLYbL6SgCQfKqNXEA0phYESPyOH9BYAlj9JMaSe0GqacdZjqnxqN7+MrLfOLYdZM6jn4IvkhofXpiC1gwANPTeySxZISLUuAMLF+OUzAOyjpi8sdGGJMuRAxHrSz1Q+yFAVLbnP3ZJoSozE2DIX8UNXGT4GpxaOEhGK1QsAQaWdBBVSBV3zvctfcVg==

Hi,

In addition to what Enrico said, there’s a resolve_one_typeclass function to try proof search on one constraint.
— Matthieu

Le lun. 15 janv. 2018 à 03:23, Enrico Tassi <enrico.tassi AT inria.fr> a écrit :

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