coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Observation about auto and family

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Jasper Stein <jasper AT codeyard.net>
Cc: mulhern <mulhern AT gmail.com>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]Observation about auto and family
Date: Mon, 30 Jan 2006 10:44:33 +0100
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:date:to:cc:subject:message-id:in-reply-to:references:x-mailer:mime-version:content-type:content-transfer-encoding:from; b=MY++C3raVQaWl5to1CDxGq5/W/QSOgmENMe7DnUIomm1aF4XpJ2n2dqNeDhVNcAKFIj5q72RJg+vIa1G+ibBC4yOWR4ynXyPyWsjVPw3mk2tfmZ4jqHFGgfm7NIFffUAOM5HSIc1DnobCDVSxz86b2YB100rgm7ER1cOUvE5uAM=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Mon, 30 Jan 2006 10:10:05 +0100 Jasper Stein
<jasper AT codeyard.net>
wrote:

> There is also the tactic "assumption" which will look in your local
> context. So instead of "auto" you might want to do "assumption; auto"
> to check for hypotheses first, and then applying auto in case it
> doesn't solve it immediately.
>
>
> Jasper Stein (Team CodeYard)

Try also the "trivial" tactic, which is also very basic.

You can also put a numerical argument to auto to fix the search depth
of auto (default = 5).

For example,

auto 1.
auto 2.

This also works for eauto.

Actually it is not exactly the search depth: the numerical argument
refers to the cost attached to tactics composed. See documentation of
auto and hints.

Cheers,

Pierre Courtieu

[Coq-Club]Observation about auto and family, mulhern
- Re: [Coq-Club]Observation about auto and family, Jasper Stein
  - Re: [Coq-Club]Observation about auto and family, Pierre Courtieu
    - Re: [Coq-Club]Observation about auto and family, mulhern