termination measure

Stream: new members

[Huỳnh Trần Khanh]

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

[Mario Carneiro]

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.