diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-02-01 16:28:41 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-02-02 18:22:15 -0500 |
| commit | 069e5cce23669707f11e59d9f68a31ad24990fe0 (patch) | |
| tree | 4f9d97e754b522bffa9eeb58e71659f25c366058 /src/PushButtonSynthesis/SaturatedSolinas.v | |
| parent | d2b8d2b69b239ffd343d87078addab0c82ad1c43 (diff) | |
More minor improvements in docstrings
Diffstat (limited to 'src/PushButtonSynthesis/SaturatedSolinas.v')
| -rw-r--r-- | src/PushButtonSynthesis/SaturatedSolinas.v | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v index 47431eb09..0e7aaf6b2 100644 --- a/src/PushButtonSynthesis/SaturatedSolinas.v +++ b/src/PushButtonSynthesis/SaturatedSolinas.v @@ -137,14 +137,18 @@ Section __. Local Notation weightf := (weight machine_wordsize 1). Local Notation evalf := (eval weightf n). - Local Notation initial_ctx := (CorrectnessStringification.dyn_context.nil). - Local Notation "'docstring_with_summary_from_lemma!' pre_extra correctness" + Local Notation notations_for_docstring + := (CorrectnessStringification.dyn_context.cons + weightf "weight" + (CorrectnessStringification.dyn_context.cons + evalf "eval" + CorrectnessStringification.dyn_context.nil))%string. + Local Notation "'docstring_with_summary_from_lemma!' summary correctness" := (docstring_with_summary_from_lemma_with_ctx! - initial_ctx - evalf - pre_extra + notations_for_docstring + summary correctness) - (only parsing, at level 10, pre_extra at next level, correctness at next level). + (only parsing, at level 10, summary at next level, correctness at next level). Definition mul := Pipeline.BoundsPipeline |