coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Enrico Tassi <enrico.tassi AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Why no unfolding on left in match?
- Date: Wed, 8 Oct 2014 22:07:06 +0200
On Wed, Oct 08, 2014 at 03:49:32PM -0400, Kevin Sullivan wrote:
> The language of pattern-valued expressions
> would need to be rich enough to support the kinds of abstraction we care
> about (probably including definition unfolding),
It cannot work in all cases, but something you may consider is writing
your own (computable) comparison function that gives you a boolean and
match on that. Computation unfolds definitions for you. More concretely,
if cmp_nat n foo then 1
else 0
The whole Mathematical Components library is built on the idea, usually
called small scale reflection, that everything that is computable is
expressed as a computable function. In other words general pattern
matching is very complex, but pattern matching over naturals is way
simpler and can be coded taking into account definition unfolding,
fixpoint computation and the like.
Best,
--
Enrico Tassi
- [Coq-Club] Why no unfolding on left in match?, Kevin Sullivan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Adam Chlipala, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Kevin Sullivan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Greg Morrisett, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Jonathan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Jonathan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Greg Morrisett, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Jonathan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Kevin Sullivan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Enrico Tassi, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Jonathan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Greg Morrisett, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Kevin Sullivan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Abhishek Anand, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Adam Chlipala, 10/08/2014
Archive powered by MHonArc 2.6.18.