5.2 Requests to the environment

5.2.1 Check term.

This command displays the type of term. When called in proof mode, the term is checked in the local context of the current subgoal.


Variants:
  1. Check num term
    Displays the type of term in the context of the num-th subgoal.

5.2.2 Eval convtactic in term.

This command performs the specified reduction on term, and displays the resulting term with its type. The term to be reduced may depend on hypothesis introduced in the first subgoal (if a proof is in progress).


Variants:
  1. Eval num convtactic in term.
    Evaluates term in the context of the num-th subgoal.

See also: section 7.5.

5.2.3 Extraction ident.

This command displays the Fw-term extracted from ident. The name ident must refer to a defined constant or a theorem. The Fw-term is extracted from the term defining ident when ident is a defined constant, or from the proof-term when ident is a theorem. The extraction is processed according to the distinction between Set and Prop; that is to say, between logical and computational content (see section 4.1.1).


Error messages:
  1. Non informative term

See also: chapter 19.1

5.2.4 Opaque ident1 ...identn.

This command forbids the unfolding of the constants ident1 ...identn by tactics using d-conversion. Unfolding a constant is replacing it by its definition.

By default, Theorem and its alternatives are stamped as Opaque. This is to keep with the usual mathematical practice of proof irrelevance: what matters in a mathematical development is the sequence of lemma statements, not their actual proofs. This distinguishes lemmas from the usual defined constants, whose actual values are of course relevant in general.
See also: sections 7.5, 7.11, 6.1.3


Error messages:
  1. ident does not exist.
    There is no constant in the environment named ident. Nevertheless, if you asked Opaque foo bar and if bar does not exist, foo is set opaque.

5.2.5 Transparent ident1 ...identn.

This command is the converse of Opaque. By default, Definition and Local declare objects as Transparent.
Warning: Transparent and Opaque are brutal and not synchronous with the reset mechanism. If a constant was transparent at point A, if you set it opaque at point B and reset to point A, you return to state of point A with the difference that the constant is still opaque. This can cause changes in tactic scripts behavior.


Error messages:
  1. Can not set transparent.
    It is a constant from a required module or a parameter.
  2. ident does not exist.
    There is no constant in the environment named ident. Nevertheless, if you give the command Transparent foo bar. and if bar does not exist, foo is set opaque.

See also: sections 7.5, 7.11, 6.1.3

5.2.6 Search ident.

This command displays the name and type of all theorems of the current context whose statement's conclusion has the form (ident t1 .. tn). This command is useful to remind the user of the name of library lemmas.

5.2.7 SearchIsos term.

SearchIsos searches terms by their type modulo isomorphism. This command displays the full name of all constants, variables, inductive types, and inductive constructors of the current context whose type is isomorphic to term modulo the contextual part of the following axiomatization (the mutual inductive types with one constructor, without implicit arguments, and for which projections exist, are regarded as a sequence of S):

1. A=Bif A¾®biB
2. Sx:A.B=Sy:A.B[x¬y]if yÏFV(Sx:A.B)
3. Px:A.B=Py:A.B[x¬y]if yÏFV(Px:A.B)
4. Sx:A.B=Sx:B.Aif xÏFV(A,B)
5. Sx:(Sy:A.B).C=Sx:A.Sy:B[y¬x].C[x¬(x,y)]
6. Px:(Sy:A.B).C=Px:A.Py:B[y¬x].C[x¬(x,y)]
7. Px:A.Sy:B.C=Sy:(Px:A.B).(Px:A.C[y¬(y x)]
8. Sx:A.unit=A
9. Sx:unit.A=A[x¬tt]
10. Px:A.unit=unit
11. Px:unit.A=A[x¬tt]

For more informations about the exact working of this command, see [30].