coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] multiple typeclass instance question

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)