diff options
Diffstat (limited to 'src/Translate.ml')
| -rw-r--r-- | src/Translate.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/Translate.ml b/src/Translate.ml index ab9ed216..ac2ee38c 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -29,8 +29,14 @@ type config = { let _ = assert_norm (FUNCTION () = Success ()) ``` *) + use_state_monad : bool; + (** If `true`, use a state-error monad. + If `false`, only use an error monad. + + Using a state-error monad is necessary when modelling I/O, for instance. + *) extract_decreases_clauses : bool; - (** If true, insert `decreases` clauses for all the recursive definitions. + (** If `true`, insert `decreases` clauses for all the recursive definitions. The body of such clauses must be defined by the user. *) |