diff options
| author | Théo Zimmermann | 2020-06-08 16:49:13 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-06-09 13:32:12 +0200 |
| commit | daddc14db590ce40bd528c5ee443c0e1d3c32cbb (patch) | |
| tree | ccb4e30c1ddb1e6239aa46cdc29fa6487c5a9186 | |
| parent | 7fa123e4380b0de201088ebbe6720a0a60a56f21 (diff) | |
Merge sections on functions and function types.
| -rw-r--r-- | doc/sphinx/language/core/assumptions.rst | 16 |
1 files changed, 6 insertions, 10 deletions
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index 9943e0aa76..955f48b772 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -44,10 +44,11 @@ fun and forall gets identical. Moreover, parentheses can be omitted in the case of a single sequence of bindings sharing the same type (e.g.: :g:`fun (x y z : A) => t` can be shortened in :g:`fun x y z : A => t`). -.. index:: fun ... => ... +.. index:: fun +.. index:: forall -Abstractions: fun ------------------ +Functions (fun) and function types (forall) +------------------------------------------- .. insertprodn term_forall_or_fun term_forall_or_fun @@ -69,11 +70,6 @@ a let-binder occurs in the list of binders, it is expanded to a let-in definition (see Section :ref:`let-in`). -.. index:: forall - -Products: forall ----------------- - The expression :n:`forall @ident : @type, @term` denotes the *product* of the variable :n:`@ident` of type :n:`@type`, over the term :n:`@term`. As for abstractions, :g:`forall` is followed by a binder list, and products @@ -92,8 +88,8 @@ Non dependent product types have a special notation: :g:`A -> B` stands for :g:`forall _ : A, B`. The *non dependent product* is used both to denote the propositional implication and function types. -Applications ------------- +Function application +-------------------- .. insertprodn term_application arg |