coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Stéphane Glondu <steph AT glondu.net>
- To: Sean Wilson <sean.wilson AT ed.ac.uk>
- Cc: Coq-Club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Automatically unfolding simple definitions
- Date: Fri, 11 Jul 2008 11:35:18 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
- Openpgp: id=FCE03DAA
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?
Cheers,
--
Stéphane Glondu
- [Coq-Club] The greatest common divisor in the standard library, Andrés Sicard-Ramírez
- Re: [Coq-Club] The greatest common divisor in the standard library, Johannes Waldmann
- [Coq-Club] Automatically unfolding simple definitions,
Sean Wilson
- Re: [Coq-Club] Automatically unfolding simple definitions,
Adam Chlipala
- Re: [Coq-Club] Automatically unfolding simple definitions, Andrew McCreight
- Re: [Coq-Club] Automatically unfolding simple definitions,
Sean Wilson
- Re: [Coq-Club] Automatically unfolding simple definitions, Vladimir Komendantsky
- Re: [Coq-Club] Automatically unfolding simple definitions, Robin Green
- Re: [Coq-Club] Automatically unfolding simple definitions, Stéphane Glondu
- Re: [Coq-Club] Automatically unfolding simple definitions,
Sean Wilson
- Re: [Coq-Club] Automatically unfolding simple definitions, Stéphane Glondu
- Re: [Coq-Club] Automatically unfolding simple definitions,
Sean Wilson
- Re: [Coq-Club] Automatically unfolding simple definitions, Benjamin Gregoire
- Re: [Coq-Club] Automatically unfolding simple definitions,
Adam Chlipala
Archive powered by MhonArc 2.6.16.