These are useful for switching between rationals and floats.
This also cleans up the implementation a bit, removing some duplicated
code.
NOTE: I am not sure if the translation from `float` to `rational`
is quite right in the what-4 backend, but I can't think of a better
way to do it at the moment.
This is semantically the same as `map` on finite sequences,
but forks a separate Haskell thread for each element of the sequence.
When the GHC runtime is instructed to use multiple OS threads,
data-parallel exeuction can be achieved.
* Add docstrings for all prelude functions and fix minor style issues.
Fixes#771
* Update `CryptolPrims` documentation
* Minor updates to the prelude
* Update CHANGES
* Updates to the cryptol book and CryptolPrims
* Fix several additional docstrings
* Specify and document properties of signed bitvector division.
Fixes#677
* Fixup test
* typos and style
* Regenerate PDFs
For the time being, there is still some information about them that
is duplicated in Cryptol.TypeCheck.TCon, but we at least the parsed syntax
does not depend on the typechecked syntax.
With the other formulation, Z3 became really bad at finding any kind
of model. Basically, it would always answer `unsat` or `unknown`.
This is undesirable, because we use models when instantiating things
at the command line. In those cases, however, we probably don't
need the rule at all... Perhaps, we should provide a way to disable
the axioms when we are looking for models?
:help with primitive types now uses vertical whitespace to match
the :help output for other types.
Help text for REPL commands can now contain linebreaks.
For quoted Cryptol syntax in docstrings, consistently use singlequotes
(') instead of backquotes (`). Backquotes are sometimes used within
the quoted code, so it's probably best to avoid using them for quotes.
Consistently capitalize and put a period at the end of docstrings.
The name "demote" is only meaningful to those who already know what
the Cryptol primitive does. Also, due to recent changes in the error
and warning messages, the name "demote" is showing up much more often
in REPL output. For example:
Defaulting type argument 'rep' of 'demote' to [2]
Showing a specific instance of polymorphic result:
* Using 'Integer' for type argument 'rep' of 'Cryptol::demote'
These messages will hopefully be made less confusing to non-experts
if the name "demote" is replaced with "number".
