diff options
author | Son Ho | 2022-02-09 13:00:47 +0100 |
---|---|---|
committer | Son Ho | 2022-02-09 13:00:47 +0100 |
commit | e161eb47d51a01e54a21c4517c85ef4c5525709e (patch) | |
tree | f8aa19f9991029085d91deb345c9567f0b13ec7a /src/Translate.ml | |
parent | 357966bc58a276906b19ea492d3d802c2b748b9e (diff) |
Add more command line arguments for the decrease clauses
Diffstat (limited to 'src/Translate.ml')
-rw-r--r-- | src/Translate.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Translate.ml b/src/Translate.ml index aa73ab7c..da0b32a4 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -24,6 +24,16 @@ type config = { let _ = assert_norm (FUNCTION () = Success ()) ``` *) + extract_decrease_clauses : bool; + (** If true, insert `decrease` clauses for all the recursive definitions. + + The body of such clauses must be defined by the user. + *) + extract_template_decrease_clauses : bool; + (** In order to help the user, we can generate "template" decrease clauses + (i.e., definitions with proper signatures but dummy bodies) in a + dedicated file. + *) } type symbolic_fun_translation = V.symbolic_value list * SA.expression |