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: Wed, 16 Mar 2016 20:29:12 +0100
- Authentication-results: mail3-smtp-sop.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-f50.google.com
- Ironport-phdr: 9a23:X6zmNRQEEUG63hbZ0mq09woBDtpsv+yvbD5Q0YIujvd0So/mwa64bBaN2/xhgRfzUJnB7Loc0qyN4/CmATZLuM/R+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq82VO18D3WPtKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayV+0CQLdZFDUrNXwurI2u7EGbDFjH2nxJeWIP2jFMHgKNuBr9R9L6tjbwnut7wiiTe8PsG+MaQzOnuo5xThb1hG88Lz8m+WrUwph5l7pavxuqpDR7wp6SeIaRJeZzdaPbfMoHSCxPRJACBGR6HoqgYt5XXKI6NuFCoty4/gNWoA==
So, this would address both of Arnaud's points below.
That was even the premise of Arnaud's points below :-) .
I find it ironic that, just as people are coming up with interesting typed alternatives to Ltac, that perhaps these alternatives would need to rely on Ltac to do typing.
Actually, that probably wouldn't be in Ltac but in the ML API which is currently powering Ltac (and is significantly better behaved, especially for non-trivial programs like this).
- Re: [Coq-Club] multiple typeclass instance question, (continued)
- 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.