coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] finer control over typeclass instance refinement
- Date: Tue, 27 Sep 2016 23:56:49 +0000
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f169.google.com
- Ironport-phdr: 9a23:yfKHZBQy0xqLcIf40QAyucJghNpsv+yvbD5Q0YIujvd0So/mwa64ZBCN2/xhgRfzUJnB7Loc0qyN4vqmADJLuMnJ8ChbNscTB1ld0YRetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1oOra9QdaK3Iyfntq/8JzLYghOmCH1IfYrdE33/k3tsZw9hpIqAaIswFOdqXxRPu9S2GlAJFSJnh+66N3mr7B59CEFmfs68MgIfr/9ZL9wGb5RFzMgPHoy/9a6nRbGRAqLoHAbVzNFwVJzHwHZ4USiDd/KuSzgu784gXHCMA==
Consider instead:
Tactic Notation "oexact'" open_constr(term) := exact term.
Tactic Notation "oexact" uconstr(term) := lazymatch goal with |- ?G => oexact' (term : G) end.
Otherwise, the following fails:
Goal 0 = 1 -> False.
oexact (fun H => match H with eq_refl => fun p => p end).
(Note that [exact] and [refine] do bidirectional typechecking.)
On Tue, Sep 27, 2016 at 7:45 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:
If you're using typeclasses, you may have run into cases where
refinement runs when you'd rather it didn't. Here are a few very simple
tactics that can help: orefine and simple orefine, which act like refine
and simple refine, except that they don't run instance refinement in holes:
Tactic Notation "oexact" open_constr(term) := exact term.
Tactic Notation "orefine" uconstr(term) := unshelve oexact term;
shelve_unifiable.
Tactic Notation "simple" "orefine" uconstr(term) := unshelve oexact term.
(*Example:*)
Variable Foo : Type.
Existing Class Foo.
Variable Foo1 : Foo.
Goal True.
refine (let f := _ : Foo in _). (*f := Foo1 : Foo*)
orefine (let g := _ : Foo in _). (*g := ?f : Foo*)
However, beware of bug 4416...
-- Jonathan
- [Coq-Club] finer control over typeclass instance refinement, Jonathan Leivent, 09/28/2016
- Re: [Coq-Club] finer control over typeclass instance refinement, Jason Gross, 09/28/2016
- Re: [Coq-Club] finer control over typeclass instance refinement, Jonathan Leivent, 09/28/2016
- Re: [Coq-Club] finer control over typeclass instance refinement, Jason Gross, 09/28/2016
Archive powered by MHonArc 2.6.18.