X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Ftac_constructor.html;fp=matita%2Fmatita%2Fhelp%2FC%2Ftac_constructor.html;h=f0818bbbfeaa8cd82fbe9d2e0d675f308991d33c;hb=d29fd4947ea4551f1fa078e56ed2a21b4515536f;hp=0000000000000000000000000000000000000000;hpb=a19551fd50df93951d78eea4c163d434f844047c;p=helm.git diff --git a/matita/matita/help/C/tac_constructor.html b/matita/matita/help/C/tac_constructor.html new file mode 100644 index 000000000..f0818bbbf --- /dev/null +++ b/matita/matita/help/C/tac_constructor.html @@ -0,0 +1,11 @@ + +constructor
constructor
Prev Chapter 7. Tactics Next

constructor

%n {args}

+

Synopsis:

% [nat] [{sterm…}]

Pre-conditions:

The conclusion of the current sequent must be + an inductive type or the application of an inductive type with + at least n constructors.

Action:

It applies the n-th constructor of the + inductive type of the conclusion of the current sequent to + the arguments args. + If n is omitted, it defaults to 1.

New sequents to prove:

It opens a new sequent for each premise of the constructor + that can not be inferred by unification. For more details, + see the apply tactic.

+

Prev Up Next
clear Home decompose
\ No newline at end of file