coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] multiple typeclass instance question
- Date: Sun, 13 Mar 2016 10:29:48 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=arnaud.spiwack AT gmail.com; spf=Pass smtp.mailfrom=arnaud.spiwack AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f48.google.com
- Ironport-phdr: 9a23:uPzrZhWC3LZ4JIaRejY8DTVzkmrV8LGtZVwlr6E/grcLSJyIuqrYZhyHt8tkgFKBZ4jH8fUM07OQ6PC/Hz1cqs7Y+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8KVMlkD3GP1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3SNp41Rr1ADTkgL3t9pIiy7UGCHkOz4S43VXxeuR5VCUCR5xbjG5z1ryHSt+xn2SDcM9egHp4uXjH3xr1tQQLkwBwfNiEw+2Kf3sVrlKNEqRmijxh+08jMZ4WEKPd1fqXcZM4XA2RbCJUCHxddC5+xOtNcR9EKOvxV+syk/wMD
Possibly. In that case we'd have a much cleaner story for tactics in terms. But this would probably be the only source of backtracking in the pretyper, if I'm not mistaken.
On 12 March 2016 at 13:51, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:
On 11/03/2016 21:58, Arnaud Spiwack wrote:
> Of course, for Coq, this is probably unworkable. Pretyping is the most
> sensitive part of Coq and making everything subtly different in
> unpredictable ways is probably not worth the huge effort this would
> represent.
I'm not sure that the pretyper by itself would be difficult to port to
the monad, at least for the pretyping.ml file. This would make it
compatible with the tactic-in-term bactracking. What would be more
difficult would be the unification stuff.
PMP
- Re: [Coq-Club] multiple typeclass instance question, (continued)
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jason Gross, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jason Gross, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jason Gross, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jason Gross, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/11/2016
- Re: [Coq-Club] multiple typeclass instance question, Pierre-Marie Pédrot, 03/12/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/13/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/13/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/15/2016
- Re: [Coq-Club] multiple typeclass instance question, Matthieu Sozeau, 03/15/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/15/2016
- Re: [Coq-Club] multiple typeclass instance question, Matthieu Sozeau, 03/15/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/16/2016
- Re: [Coq-Club] multiple typeclass instance question, Matthieu Sozeau, 03/16/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/13/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/16/2016
Archive powered by MHonArc 2.6.18.