diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/core/variants.rst | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst index fc2481201f..d8fba5bc3d 100644 --- a/doc/sphinx/language/core/variants.rst +++ b/doc/sphinx/language/core/variants.rst @@ -1,3 +1,30 @@ +Variants and the `match` construct +================================== + +Variants +-------- + +.. cmd:: Variant @variant_definition {* with @variant_definition } + + .. insertprodn variant_definition variant_definition + + .. prodn:: + variant_definition ::= @ident_decl {* @binder } {? %| {* @binder } } {? : @type } := {? %| } {+| @constructor } {? @decl_notations } + + The :cmd:`Variant` command is similar to the :cmd:`Inductive` command, except + that it disallows recursive definition of types (for instance, lists cannot + be defined using :cmd:`Variant`). No induction scheme is generated for + this variant, unless the :flag:`Nonrecursive Elimination Schemes` flag is on. + + This command supports the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`universes(template)`, + :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, + :attr:`universes(noncumulative)` and :attr:`private(matching)` + attributes. + + .. exn:: The @num th argument of @ident must be @ident in @type. + :undocumented: + Private (matching) inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |