The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

On Friday 11 July 2008 10:35:18 Stéphane Glondu wrote:
> Sean Wilson wrote:
> > Definition permutation x y := forall n, count n x = count n y.
> >
> > In my domain, it is normally required that all 'simple' definitions like
> > this (i.e. non-recursive functions) be unfolded first for my automation
> > to work. As a simple example of what I need, given this definition:
>
> Have you tried "Hint Unfold permutation." after your definition?

Hi,

I was looking for a way for this to happen automatically without me having to 
explicitly name definitions. It isn't a huge burden on the user to identify 
such terms, but I wanted to remove the need for such hints if possible. I 
suppose another approach is to have the machine identify definitions that are 
suitable as unfold hints and automatically add them as unfold hints at the 
point such definitions are entered into Coq. I could then use  
Matthieu's "autosimpl" to unfold them.

Thanks,

Sean