diff options
| author | Clément Pit-Claudel | 2019-10-06 22:19:07 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-10-06 22:19:07 -0400 |
| commit | ef7cade43d514cb8f3d6022c298fdc467fcc4a33 (patch) | |
| tree | 010c9920c5b4b0dd5758cc53ea50f12da314f338 | |
| parent | 8ecc5555b1b79ec2278cd9d425dab6c209139c3a (diff) | |
| parent | 817b32d7a01dea3988f25e1130ffbb2d091837b3 (diff) | |
Merge PR #10834: Fix #10831: minor issues in documentation of Function.
Reviewed-by: cpitclaudel
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index dc4f91e66b..2d047a1058 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -638,7 +638,11 @@ the induction principle to easily reason about the function. than like this: - .. coqtop:: reset all + .. coqtop:: reset none + + Require Import FunInd. + + .. coqtop:: all Function plus (n m : nat) {struct n} : nat := match n with @@ -649,17 +653,22 @@ the induction principle to easily reason about the function. *Limitations* -|term_0| must be built as a *pure pattern matching tree* (:g:`match … with`) +:token:`term` must be built as a *pure pattern matching tree* (:g:`match … with`) with applications only *at the end* of each branch. Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the presence of partial application of :g:`wrong` in the body of :g:`wrong`: -.. coqtop:: all +.. coqtop:: none + + Require List. + Import List.ListNotations. + +.. coqtop:: all fail - Fail Function wrong (C:nat) : nat := - List.hd 0 (List.map wrong (C::nil)). + Function wrong (C:nat) : nat := + List.hd 0 (List.map wrong (C::nil)). For now, dependent cases are not treated for non structurally terminating functions. |