From b0e3404de4dff81680861517f70c496af1d92bbc Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 13 May 2020 19:48:08 +0200 Subject: Create a new file on Variants. --- doc/sphinx/language/core/variants.rst | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 doc/sphinx/language/core/variants.rst (limited to 'doc/sphinx/language/core') diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst new file mode 100644 index 0000000000..fc2481201f --- /dev/null +++ b/doc/sphinx/language/core/variants.rst @@ -0,0 +1,24 @@ +Private (matching) inductive types +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. attr:: private(matching) + + This attribute can be used to forbid the use of the :g:`match` + construct on objects of this inductive type outside of the module + where it is defined. There is also a legacy syntax using the + ``Private`` prefix (cf. :n:`@legacy_attr`). + + The main use case of private (matching) inductive types is to emulate + quotient types / higher-order inductive types in projects such as + the `HoTT library `_. + +.. example:: + + .. coqtop:: all + + Module Foo. + #[ private(matching) ] Inductive my_nat := my_O : my_nat | my_S : my_nat -> my_nat. + Check (fun x : my_nat => match x with my_O => true | my_S _ => false end). + End Foo. + Import Foo. + Fail Check (fun x : my_nat => match x with my_O => true | my_S _ => false end). -- cgit v1.2.3