X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_constructor.html;fp=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_constructor.html;h=0000000000000000000000000000000000000000;hb=223f17d088cd8bf01f9314580fc34e66256841ac;hp=9fc2a8b253d5f05d296fd15917275593d0508280;hpb=18ca6cec5a82241cc389bbf82742565e79d81ed8;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_constructor.html b/helm/www/matita/docs/manual/tac_constructor.html deleted file mode 100644 index 9fc2a8b25..000000000 --- a/helm/www/matita/docs/manual/tac_constructor.html +++ /dev/null @@ -1,10 +0,0 @@ - - -constructor nat
constructor nat
Prev Chapter 6. Tactics Next

constructor nat

constructor n

-

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.

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
change <pattern> with sterm Home contradiction