Skip to content

3.2.0

Latest
Latest
Compare
Choose a tag to compare
@mccleeary-galois mccleeary-galois released this 20 Aug 17:29
· 63 commits to master since this release
3.2.0
1bcb75c

Language changes

  • Add implicit imports for non-anonymous modules defined by functor
    instantiation. For details, see #1691.

Bug fixes

  • Fix #1685, which caused Cryptol to panic when given a local definition without
    a type signature that uses numeric constraint guards.

  • Fix #1593 and #1693, two related bugs that would cause Cryptol to panic when
    checking ill-typed constraint guards for exhaustivity.

  • Fix #1675, which could cause PrimeEC to produce incorrect results.

  • Fix #1489, which allows for the type checker to reason about exponents.

New features

  • New REPL command :focus enables specifying a submodule scope for evaluating
    expressions.

    :focus submodule M
:browse

  • New REPL command :check-docstrings extracts code-blocks from docstring
    comments from a module. Code blocks can be delimited with three-or-more
    backticks using the language "repl". Code blocks are evaluated in a local
    REPL context and checked to pass.

    /**
 * ```repl
 * :exhaust f
 * ```
 */
f : [8] -> Bool
f x = x + 1 - 1 == x
Assets 24
Loading