Commit Graph

69 Commits

Author SHA1 Message Date
Brian Huffman
ddfe615a14 Document :exhaust command in the cryptol book. Fixes #466. 2018-05-22 15:17:15 -07:00
Brian Huffman
6fdc1ff326 Write about type constraint synonyms in Programming Cryptol.
Fixes #452.
2018-03-22 16:06:55 -07:00
Brian Huffman
fccf55f30f Remove obsolete cvs-era $Header$ keywords. 2018-03-22 13:33:12 -07:00
Brian Huffman
e84dcc5126 Document logical connectives (==>, /\, \/) in Programming Cryptol book. 2017-10-05 14:17:51 -07:00
Brian Huffman
fd9e003cd3 More documentation for REPL commands :browse and :help. 2017-10-05 13:51:50 -07:00
Brian Huffman
59a34a4624 Update table of Cryptol primitives with new type constraints. 2017-10-05 11:29:21 -07:00
Brian Huffman
11067f8220 Document new type classes Zero, Logic, and SignedCmp. Fixes #451. 2017-10-05 11:15:49 -07:00
Brian Huffman
361be3827e Fix incorrect spacing after abbreviation "vs." 2017-10-05 11:08:34 -07:00
Brian Huffman
6d484c854d Fix inaccurate statements about Cmp class. 2017-10-05 10:38:37 -07:00
Brian Huffman
1909e9ca51 In Programming Cryptol table of contents, make entire lines clickable links. 2017-10-05 10:24:23 -07:00
Brian Huffman
ffe113669e Document the REPL let-definition feature. Fixes #359. 2017-10-05 10:23:34 -07:00
Brian Huffman
7b0b8836c0 Fix outdated reference to inf a constraint in docs. 2017-10-05 10:20:57 -07:00
Brian Huffman
0478ec434c Uniformly place footnotes after punctuation. 2017-10-05 09:25:44 -07:00
Brian Huffman
1e453436b2 Fix grammatical errors in manuals 2017-08-02 19:46:26 -07:00
Aaron Tomb
77db35ffda Document success and error exit codes. 2017-03-21 09:08:48 -07:00
Aaron Tomb
c025f874db Document the prover-stats option. 2017-03-21 09:06:18 -07:00
Robert Dockins
cd9ffed00b Update examples to use (/\) instead of (&&) where appropriate,
and to squash other warnings related to the upcomming precedence change.
2016-08-22 18:14:44 -07:00
Robert Dockins
f6f1d84770 Update the Cryptol documentation with the new 'update' primitives 2016-08-12 16:18:11 -07:00
Brian Huffman
a8eccb9db7 Fix some incorrect syntax in Programming Cryptol appendix 2016-08-04 14:36:33 -07:00
Brian Huffman
e868e78601 Update precedence table to match Cryptol prelude 2016-08-04 14:33:41 -07:00
Brian Huffman
c537b5a1cd Small fixes for "Programming Cryptol" appendices 2016-08-04 10:54:11 -07:00
Brian Huffman
5bca2a5560 Fix lots of wrong types for primitives in appendix B 2016-08-03 16:18:31 -07:00
Brian Huffman
ed1dd212ab More small fixes in Programming Cryptol 2016-08-03 16:04:10 -07:00
Brian Huffman
4cc76e6c8b Small fixes for crash-course chapter of Programming Cryptol
Changes include spelling, grammar, punctuation,
typesetting, and code formatting. A few factual errors
have been fixed, and some Cryptol REPL output has been
updated as well.
2016-08-03 09:54:52 -07:00
Robert Dockins
c60be15873 Add 'trace' and 'traceVal' to the primitive operations lists in the documentation. 2016-07-13 14:21:29 -07:00
Brian Huffman
c2e0cc5839 Remove unused AES functions. Fixes #352. 2016-07-07 14:40:08 -07:00
Adam C. Foltzer
054a3e2248 instantiate Scytale diameter
Fixes #349
2016-07-05 14:42:59 -07:00
Adam C. Foltzer
2c428804bc remove splitBy and update documentation
Closes #291
2016-07-05 09:58:49 -07:00
Dylan McNamee
ab279f01d5 incorporating typos and other improvements to docs 2016-04-27 11:52:09 -07:00
Dylan McNamee
b92cdcccda file cleanup 2016-04-21 13:54:52 -07:00
Dylan McNamee
04e22d8dd6 command appendix 2016-04-21 13:53:02 -07:00
Dylan McNamee
623b847094 merging changes to docs 2016-04-19 11:41:55 -07:00
Joseph Kiniry
0ba8d97c8a Removed extra 's'. 2016-04-18 15:16:39 -07:00
Joseph Kiniry
849fecead8 Merge branch 'master' of github.com:GaloisInc/cryptol 2016-04-18 15:15:58 -07:00
Joseph Kiniry
d43fcc9ebe Whitespace tweak. 2016-04-18 15:15:56 -07:00
Thomas M. DuBuisson
bd593e4ebe
Add hierarchy to the module documentation. 2016-02-25 16:34:30 -08:00
Dylan McNamee
86c3d0ffe2 Module documentation 2016-02-25 15:14:00 -08:00
Brian Huffman
1322156d28 Remove trailing whitespace 2016-02-19 10:08:20 -08:00
Adam C. Foltzer
4d3fc9a413 Update copyright dates and add missing headers 2016-01-19 18:19:35 -08:00
Joseph Kiniry
357905934b Merge branch 'master' of github.com:GaloisInc/cryptol 2016-01-03 23:46:52 -08:00
Adam C. Foltzer
9c07fe1006 merge in the 2.2.6 changes, including z3 switch 2015-12-23 16:10:56 -08:00
Adam C. Foltzer
3ae0dda7ac switch to Z3 for typechecking and proving
Note: the hardcoding in this patch is only for the 2.2 hotfix branch; in
the 2.3 branch we will only have to change the default setting for the
typechecker.
2015-12-23 14:59:10 -08:00
Adam C. Foltzer
4c441898d9 remove a merge error from docs Makefile 2015-10-05 15:33:04 -07:00
Adam C. Foltzer
baddfcaab8 Merge branch 'heads/hotfixes/v2.2.5' 2015-10-01 10:56:30 -07:00
Adam C. Foltzer
7d81568555 remove iteSolver option for compat with sbv 5+ 2015-09-30 14:24:21 -07:00
Jenkins Builder
75539f9244 add \protect to fix error on Windows docs 2015-09-16 13:12:37 -07:00
Adam C. Foltzer
2ca0e6f732 switch back to non-latexmk for book (Windows)
Windows didn't like the latexmk solution from
5eb5f00d0a.
2015-09-16 11:37:00 -07:00
Adam C. Foltzer
5eb5f00d0a change how the book is built 2015-09-15 13:38:06 -07:00
Dylan McNamee
c27c91af3a fixed negative stepped sequence example (issue #234) in ProgrammingCryptol 2015-06-05 12:02:16 -07:00
Joseph Kiniry
6af66f2dba Merge branch 'master' of github.com:GaloisInc/cryptol 2015-05-04 15:19:39 -07:00