X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Ftac_cases.html;fp=matita%2Fmatita%2Fhelp%2FC%2Ftac_cases.html;h=0000000000000000000000000000000000000000;hb=9d5a0d55e331b348d44b6d50d3d67e62b60a0e18;hp=646281d846932c9840a6da8cd5d2dce1124608f6;hpb=7b6ca76a0ed511b288b654729c9758277dbcd352;p=helm.git diff --git a/matita/matita/help/C/tac_cases.html b/matita/matita/help/C/tac_cases.html deleted file mode 100644 index 646281d84..000000000 --- a/matita/matita/help/C/tac_cases.html +++ /dev/null @@ -1,23 +0,0 @@ - -cases
cases
Prev Chapter 7. Tactics Next

cases

- cases t pattern -

-

Synopsis:

- cases - term pattern -

Pre-conditions:

- t must inhabit an inductive type -

Action:

- It proceed by cases on t. The new generated - hypothesis in each branch are named according to - hyps. - The elimintation predicate is restricted by - pattern. In particular, if some hypothesis - is listed in pattern, the hypothesis is - generalized and cleared before proceeding by cases on - t. Currently, we only support patterns of the - form H1 … Hn ⊢ %. This limitation will be lifted in the future. -

New sequents to prove:

One new sequent for each constructor of the type of - t. Each sequent has a new hypothesis for - each argument of the constructor.

-

Prev Up Next
assumption Home change
\ No newline at end of file