6.3 Displaying information

6.3.1 Show.

This command displays the current goals.


Variants:
  1. Show num.
    Displays only the num-th subgoal.

    Error messages:
    1. No such goal
    2. No focused proof

  2. Show Implicits.
    Displays the current goals, printing the implicit arguments of constants.

  3. Show Implicits num.
    Same as above, only displaying the num-th subgoal.

  4. Show Script.
    Displays the whole list of tactics applied from the beginning of the current proof. This tactics script may contain some holes (subgoals not yet proved). They are printed under the form <Your Tactic Text here>.

  5. Show Tree.
    This command can be seen as a more structured way of displaying the state of the proof than that provided by Show Script. Instead of just giving the list of tactics that have been applied, it shows the derivation tree constructed by then. Each node of the tree contains the conclusion of the corresponding sub-derivation (i.e. a goal with its corresponding local context) and the tactic that has generated all the sub-derivations. The leaves of this tree are the goals which still remain to be proved.

  6. Show Proof.
    It displays the proof term generated by the tactics that have been applied. If the proof is not completed, this term contain holes, which correspond to the sub-terms which are still to be constructed. These holes appear as a question mark indexed by an integer, and applied to the list of variables in the context, since it may depend on them. The types obtained by abstracting away the context from the type of each hole-placer are also printed.

  7. Show Conjectures.
    It prints the list of the names of all the theorems that are currently being proved. As it is possible to start proving a previous lemma during the proof of a theorem, this list may contain several names.

  8. Show Intro.
    If the current goal begins by at least one product, this command prints the name of the first product, as it would be generated by an anonymous Intro. The aim of this command is to ease the writing of more robust scripts. For example, with an appropriate Proof General macro, it is possible to transform any anonymous Intro into a qualified one such as Intro y13. In the case of a non-product goal, it prints nothing.

  9. Show Intros.
    This command is similar to the previous one, it simulates the naming process of an Intros.

6.3.2 Set Hyps_limit num.

This command sets the maximum number of hypotheses displayed in goals after the application of a tactic. All the hypotheses remains usable in the proof development.

6.3.3 Unset Hyps_limit.

This command goes back to the default mode which is to print all available hypotheses.