From 405ec7a431ba7d9673e753b4fa3bc013836f3aca Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 10 Dec 2021 10:08:01 -0800 Subject: [PATCH] Remove outdated syntax information --- inductive_types.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/inductive_types.rst b/inductive_types.rst index 303dbe6..8084870 100644 --- a/inductive_types.rst +++ b/inductive_types.rst @@ -15,7 +15,7 @@ Intuitively, an inductive type is built up from a specified list of constructors ... | constructorₙ : ... → foo -The intuition is that each constructor specifies a way of building new objects of ``foo``, possibly from previously constructed values. The type ``foo`` consists of nothing more than the objects that are constructed in this way. The first character ``|`` in an inductive declaration is optional. We can also separate constructors using a comma instead of ``|``. +The intuition is that each constructor specifies a way of building new objects of ``foo``, possibly from previously constructed values. The type ``foo`` consists of nothing more than the objects that are constructed in this way. When a constructor has the type ``foo``, the ``: foo`` giving the type of the constructor can be omitted (which is useful in enumerated types). We will see below that the arguments to the constructors can include objects of type ``foo``, subject to a certain "positivity" constraint, which guarantees that elements of ``foo`` are built from the bottom up. Roughly speaking, each ``...`` can be any Pi type constructed from ``foo`` and previously defined types, in which ``foo`` appears, if at all, only as the "target" of the Pi type. For more details, see [Dybj94]_.