Rob Dockins
d740442035
Update documenetation with new enumeration forms,
...
and update the reference semantics.
Other minor documentation fixes and updates.
2021-07-20 17:01:50 -07:00
Rob Dockins
976468dce7
Fix typos
2021-01-12 11:20:57 -08:00
Rob Dockins
557b928caf
Update syntax and semantics documents with newtype changes
2021-01-12 11:18:58 -08:00
Brian Huffman
36b8bd2e07
Fix miscellaneous typos in Syntax.md.
2020-10-13 11:09:51 -07:00
Brian Huffman
a23267fe3d
More accurate descriptions for lg2 and width in book appendix.
...
Fixes #931 .
2020-10-13 10:53:32 -07:00
Brian Huffman
e08cac3828
Remove redundant word "Size" in table of built-in type-level operators.
...
We have decided to avoid the term "size type" in favor of
"numeric type" (#597 ), and the word is uninformative in this
context anyway.
2020-10-13 10:39:25 -07:00
Iavor Diatchki
39acf61ee5
Update documentation with info about floats + fractional literals
2020-07-14 15:36:37 -07:00
Brett Boston
0e35995ee4
Document element type constraints for enumerations
2020-07-08 10:13:55 -07:00
Brett Boston
a87684aad4
Clarify that each file can only contain a single module
2020-06-30 19:10:33 -07:00
Brett Boston
f742b1614a
Document polynomial syntax + escape pipes in Version2Table
2020-06-26 15:32:47 -07:00
Iavor Diatchki
2219aca55c
Document lifted selectors.
...
Fixes #303
2020-05-05 14:59:45 -07:00
Brian Huffman
8d2f1ed2ba
Add examples of x @ i = e syntax to Syntax.md.
2019-06-19 11:25:30 -07:00
Brian Huffman
088126076e
Remove trailing whitespace.
2019-06-19 11:24:59 -07:00
Iavor Diatchki
d428f64bdc
Add some examples about how to write Cryptol expressions.
2019-05-30 10:29:35 -07:00
Iavor Diatchki
afe89d2ad4
Add examples of doing record updates
2019-03-01 11:10:28 -08:00
Brian Huffman
e59c9abfbb
Remove [x..] and [x,y..] syntax from documentation.
2019-02-28 10:38:38 -08:00
Iavor Diatchki
6a8c6c3134
Update Syntax.md and re-sync it with Syntax.tex
...
Note that Syntax.tex should be generated automatically
2019-02-18 17:20:01 -08:00
Brian Huffman
863c165c66
Update syntax appendix of Cryptol book.
2018-07-20 18:13:15 -07:00
Iavor S. Diatchki
2faa44e17b
Add some documentation for the module system.
2017-10-26 16:34:08 -07:00
Rob Dockins
d32f3324c9
Update syntax reference with new fixity information for (||) and (&&)
2017-10-02 18:17:38 -07:00
Robert Dockins
9550d1b8dd
Update syntax documentation
2017-08-16 18:22:49 -07:00
Brian Huffman
1e453436b2
Fix grammatical errors in manuals
2017-08-02 19:46:26 -07:00
Robert Dockins
f6f1d84770
Update the Cryptol documentation with the new 'update' primitives
2016-08-12 16:18:11 -07:00
Dylan McNamee
ab279f01d5
incorporating typos and other improvements to docs
2016-04-27 11:52:09 -07:00
Dylan McNamee
aa1565bac4
documentation fixes (tuples, spelling, other wibble)
2015-05-05 08:38:43 -07:00
Adam C. Foltzer
284338c938
Add the mono-binds flag
...
When `:set mono-binds=on`, any local definitions lacking type
signatures will not be generalized (i.e., will be monomorphic). This
reduces what is in most cases unnecessary polymorphism that can give
rise to constraints that are difficult to solve. This also improves
the performance of the Cryptol interpreter by lifting many polymorphic
type applications out of the inner loops that are commonly defined as
bindings in `where` clauses.
The flag is on by default in the Cryptol REPL, and in most cases makes
it possible to leave out more type signatures in `where` clauses than
before. However, some programs really do rely on inferring polymorphic
types for local variables; in this case adding an explicit polymorphic
type signature to the local binding in question will make the program
typecheck.
2014-12-15 17:48:25 -08:00
Dylan McNamee
0e29d1d369
issue 108 from Sean, and a minor tweak to the AES chapter's formatting.
2014-09-17 12:28:30 -07:00
Adam C. Foltzer
15e6fec34d
update documentation for #82
2014-09-09 11:59:39 -04:00
Dylan McNamee
288178dea2
markdown -> .md, Acks section, adding spec to contrib
2014-04-23 13:15:18 -07:00
