sail/lib/isabelle/output, branch sail2 Formal specification language for ISAs Remove generated TeX file 2019-05-08T10:46:11+00:00 Thomas Bauereiss 2019-05-08T10:45:45+00:00 611748f32de5269eb3d56bb3098cf07c9a89a0ba 






Basic loop termination measures for Coq
2019-04-15T11:08:28+00:00

Brian Campbell

2019-04-15T11:08:28+00:00

1f421b865a87a161a82550443a0cf39aa2642d9c

Currently only supports pure termination measures for loops with effects.

The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).





Currently only supports pure termination measures for loops with effects.

The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).