GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-10-04 09:28:58 +03:00
Code Issues Projects Releases Wiki Activity

Clarify "Known Enum Type" restriction in RefMan

Browse Source
This commit is contained in:
Ryan Scott 2024-02-01 16:24:01 -05:00
parent c8e4615307
commit 2f5bbd97bd
1 changed files with 10 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
docs/RefMan/TypeDeclarations.rst
View File

@ -164,11 +164,9 @@ constructor:
Nothing -> True
**The Matched Expression Must Have a Known Enum Type.** Cryptol will reject
the definition of ``f``, where ``f`` lacks a type signature, or is not not
an ``enum`` type.
the following definition of ``f``, where ``f`` lacks a type signature:
.. code-block:: cryptol
f x =
case x of
_ -> ()
@ -184,3 +182,12 @@ anything about the type of ``x``. It would be incorrect to give ``f`` this type:
This is because ``f`` is not really polymorphic in its argument type, as the
only values that can be matched in a ``case`` expression are those whose type
was declared as an ``enum``. As such, Cryptol rejects this example.
Cryptol will also reject this definition, where the type of the value
being matched is not an ``enum`` type:
.. code-block:: cryptol
g : Integer -> ()
g x =
case x of
_ -> ()