Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] multiple typeclass instance question

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] multiple typeclass instance question


Chronological Thread 
  • 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).




Archive powered by MHonArc 2.6.18.

Top of Page