helm/www/matita/docs/manual-0.5.9/tac_lapply.html

   1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
   2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>lapply</title><link rel="stylesheet" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets V1.78.1" /><link rel="home" href="index.html" title="Matita V0.5.9 User Manual (rev. 0.5.9 )" /><link rel="up" href="sec_tactics.html" title="Chapter 7. Tactics" /><link rel="prev" href="tac_inversion.html" title="inversion" /><link rel="next" href="tac_left.html" title="left" /></head><body><a xmlns="" href="../../../"><div class="matita_logo"><img src="figures/matita.png" alt="Tiny Matita logo" /><span>Matita Home</span></div></a><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">lapply</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_inversion.html">Prev</a> </td><th width="60%" align="center">Chapter 7. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_left.html">Next</a></td></tr></table><hr /></div><div class="sect1"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_lapply"></a>lapply</h2></div></div></div><p><strong class="userinput"><code>
   3      lapply linear depth=d t
   4      to t<sub>1</sub>, ..., t<sub>n</sub> as H
   5     </code></strong></p><p>
   6       </p><div class="variablelist"><dl class="variablelist"><dt><span class="term">Synopsis:</span></dt><dd><p>
   7              <span class="bold"><strong>lapply</strong></span>
   8              [<span class="bold"><strong>linear</strong></span>]
   9              [<span class="bold"><strong>depth=</strong></span><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span>]
  10              <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span>
  11              [<span class="bold"><strong>to</strong></span>
  12               <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span>
  13               [<span class="bold"><strong>,</strong></span><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.sterm">sterm</a></em></span>…]
  14              ]
  15              [<span class="bold"><strong>as</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span>]
  16             </p></dd><dt><span class="term">Pre-conditions:</span></dt><dd><p>
  17              <span class="command"><strong>t</strong></span> must have at least <span class="command"><strong>d</strong></span>
  18              independent premises and <span class="command"><strong>n</strong></span> must not be
  19              greater than <span class="command"><strong>d</strong></span>.
  20             </p></dd><dt><span class="term">Action:</span></dt><dd><p>
  21              Invokes <span class="command"><strong>letin H ≝ (t ? ... ?)</strong></span>
  22              with enough <span class="command"><strong>?</strong></span>'s to reach the
  23              <span class="command"><strong>d</strong></span>-th independent premise of
  24              <span class="command"><strong>t</strong></span>
  25              (<span class="command"><strong>d</strong></span> is maximum if unspecified).
  26              Then istantiates (by <span class="command"><strong>apply</strong></span>) with
  27              t<sub>1</sub>, ..., t<sub>n</sub>
  28              the <span class="command"><strong>?</strong></span>'s corresponding to the first
  29              <span class="command"><strong>n</strong></span> independent premises of
  30              <span class="command"><strong>t</strong></span>.
  31              Usually the other <span class="command"><strong>?</strong></span>'s preceding the
  32              <span class="command"><strong>n</strong></span>-th independent premise of
  33              <span class="command"><strong>t</strong></span> are istantiated as a consequence.
  34              If the <span class="command"><strong>linear</strong></span> flag is specified and if
  35              <span class="command"><strong>t, t<sub>1</sub>, ..., t<sub>n</sub></strong></span>
  36              are (applications of) premises in the current context, they are
  37              <span class="command"><strong>clear</strong></span>ed.
  38             </p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>
  39              The ones opened by the tactics <span class="command"><strong>lapply</strong></span> invokes.
  40             </p></dd></dl></div><p>
  41     </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_inversion.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_left.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">inversion </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> left</td></tr></table></div></body></html>