{"action":"opened","issue":{"url":"https://api.github.com/repos/gmalecha/coq-with-hint-db/issues/2","labels_url":"https://api.github.com/repos/gmalecha/coq-with-hint-db/issues/2/labels{/name}","comments_url":"https://api.github.com/repos/gmalecha/coq-with-hint-db/issues/2/comments","events_url":"https://api.github.com/repos/gmalecha/coq-with-hint-db/issues/2/events","html_url":"https://github.com/gmalecha/coq-with-hint-db/issues/2","id":129559562,"number":2,"title":"Add an option to filter hints with a given pattern","user":{"login":"jeremie-koenig","id":290805,"avatar_url":"https://avatars.githubusercontent.com/u/290805?v=3","gravatar_id":"","url":"https://api.github.com/users/jeremie-koenig","html_url":"https://github.com/jeremie-koenig","followers_url":"https://api.github.com/users/jeremie-koenig/followers","following_url":"https://api.github.com/users/jeremie-koenig/following{/other_user}","gists_url":"https://api.github.com/users/jeremie-koenig/gists{/gist_id}","starred_url":"https://api.github.com/users/jeremie-koenig/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jeremie-koenig/subscriptions","organizations_url":"https://api.github.com/users/jeremie-koenig/orgs","repos_url":"https://api.github.com/users/jeremie-koenig/repos","events_url":"https://api.github.com/users/jeremie-koenig/events{/privacy}","received_events_url":"https://api.github.com/users/jeremie-koenig/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":0,"created_at":"2016-01-28T19:47:40Z","updated_at":"2016-01-28T19:47:40Z","closed_at":null,"body":"Maybe it would be nice to be able to specify a pattern for filtering the results by their type (or rather, their conclusion), as in:\r\n\r\n    plus_of [ db:typeclass_instances ] matching (Proper ?R f) run (fun H => eapply H).\r\n    foreach [ * |- ] matching (eq _ _) run (fun H => erewrite ?H; clear H).\r\n\r\nOf course the user could always do the filtering themselves with `lazymatch` in the tactic expression. But keep in mind they would need to extract the conclusion first (assuming that's what they're interested in), and I suspect a direct implementation might be more efficient, especially for discriminated hint databases that have lots of things in them such as `typeclass_instances`.\r\n\r\nA fancier version would be to have \"collection expressions\" like:\r\n\r\n    foreach [ (* |-, db:core) matching (eq _ _), db:rewrite_rules ] (fun H => rewrite ?H)."}}