Zulip Chat Archive

Stream: new members

Topic: termination measure


view this post on Zulip Huỳnh Trần Khanh (Feb 14 2021 at 03:19):

is there something in lean equivalent to 'termination measure' in coq and dafny?

view this post on Zulip 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