Stream: new members
Topic: termination measure
Huỳnh Trần Khanh (Feb 14 2021 at 03:19):
is there something in lean equivalent to 'termination measure' in coq and dafny?
Mario Carneiro (Feb 14 2021 at 03:23):
Not exactly. You can prove things and construct definitions by well founded recursion, which uses a default size measure that you can override with a measure function of your own, or even a more complicated well founded relation. The usual compilation strategy doesn't use well founded recursion but instead a kind of structural recursion that permits nested constructor applications; this is the nearest analogue of Coq's termination checker, but it's compiled down to recursors instead of axiomatized.
Last updated: May 14 2021 at 14:20 UTC