Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Why no unfolding on left in match?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Why no unfolding on left in match?


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



Archive powered by MHonArc 2.6.18.

Top of Page