Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Automatically unfolding simple definitions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Automatically unfolding simple definitions


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






Archive powered by MhonArc 2.6.16.

Top of Page