coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: Unfold opposite

From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>
To: "Emer Ni Dhomhnaill" <emernd AT hotmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: Unfold opposite
Date: Thu, 22 Feb 2001 14:08:48 +0100 (MET)

Emer Ni Dhomhnaill writes:

> My name is Emer and I'm implementing a three-valued logic using coq. This
> is
> probably a very easy question but does there exist a tactic that can
> refold
> definitions... the opposite to the tactic unfold?

Yes, there is a "Fold" tactic.


http://coq.inria.fr/doc/node.1.2.4.html#@tactic33

--
Jean-Christophe FILLIATRE

mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr

Unfold opposite, Emer Ni Dhomhnaill
- Re: Unfold opposite, Jean-Christophe Filliatre