diff options
Diffstat (limited to 'model/postlude')
| -rw-r--r-- | model/postlude/step.sail | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/model/postlude/step.sail b/model/postlude/step.sail index e8a800f..7bf3cc5 100644 --- a/model/postlude/step.sail +++ b/model/postlude/step.sail @@ -296,3 +296,13 @@ function loop () : unit -> unit = { } } } + +// Termination measures for loops are not supported by the Lean backend, so they +// should be guarded by this condition: +$iftarget coq + +// The top-level loop isn't terminating, but we put a limit so that it can still +// be included in the Coq output +termination_measure loop while 100 + +$endif |