diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-19 10:30:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-02 19:25:22 +0200 |
| commit | 880fee8f80503fc8a40e2e07b565cfd2a99d24da (patch) | |
| tree | 67222b783e941aa265a425e1d9162a8c81d8538c /doc/sphinx/proof-engine/tactics.rst | |
| parent | fd146ca38202c9843b4240cbdac0ae75f57e4d67 (diff) | |
Make "intro"/"intros" progress on existential variables.
Diffstat (limited to 'doc/sphinx/proof-engine/tactics.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index a3d06ae04..6c1b1c08c 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -634,7 +634,12 @@ puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` or ``n`` is such that ``Hn`` or ``Xn`` is a fresh identifier. In both cases, the new subgoal is :g:`U`. -If the goal is neither a product nor starting with a let definition, +If the goal is an existential variable, ``intro`` forces the resolution of the +existential variable into a dependent product :math:`\forall`:g:`x:?X, ?Y`, puts +:g:`x:?X` in the local context and leaves :g:`?Y` as a new subgoal allowed to +depend on :g:`x`. + +If the goal is neither a product, nor starting with a let definition, nor an existential variable, the tactic ``intro`` applies the tactic ``hnf`` until the tactic ``intro`` can be applied or the goal is not head-reducible. |