coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]conversion tactics

From: "Ethan Aubin" <ethan.aubin AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club]conversion tactics
Date: Sat, 10 Jun 2006 10:39:59 -0400
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:to:subject:mime-version:content-type:content-transfer-encoding:content-disposition; b=gZhUCM5khIBQ2+sQMJ6XGLw70Z2EpX++CS1AEdPQI5wqwTtmyxdZ3S8z28oGMU6p/NsF1EsUZI+0DlCxRRc8PGNqDjqrpvkGIkOjVCPVZFryt3rG6O327ycQMaAWuFhjXb34z8ZzhGB5qv3WJojsHfy7ntVN2GxVtHAAe2V1GWI=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi, Is it possible to perform a single step of delta/beta/etc
reduction via a tactic? Is the evaulation order of the conversion
tactics (or CiC) specified? Also, whats the best forum to ask novice
questions? Thanks - Ethan

[Coq-Club]conversion tactics, Ethan Aubin
- Re: [Coq-Club]conversion tactics, Pierre Courtieu