docs/rosette: Fix inline code

This commit is contained in:
Krystine Sherwin 2025-02-27 16:11:44 +13:00
parent c429aef60f
commit db823a6acb
No known key found for this signature in database
1 changed files with 1 additions and 1 deletions

View File

@ -386,7 +386,7 @@ and the ``next_state`` in a single variable. Iteration over all of the
} }
For the ``write_initial`` method, the SMT-LIB backend uses ``declare-const`` and For the ``write_initial`` method, the SMT-LIB backend uses ``declare-const`` and
`assert`\ s which must always hold true. For Rosette we instead define the ``assert``\ s which must always hold true. For Rosette we instead define the
initial state as any other variable that can be used by external code. This initial state as any other variable that can be used by external code. This
variable, ``[name]_initial``, can then be used in the ``[name]`` function call; variable, ``[name]_initial``, can then be used in the ``[name]`` function call;
allowing the Rosette code to be used in the generation of the ``next_state``, allowing the Rosette code to be used in the generation of the ``next_state``,