Missing termination metric

There is a function.

fun foo ():<> void

If I mix declaration and definition in dats, the compiler complains about
missing termination metric.

fun foo ():<> void = ()

However, if I separate them, it compiles fine.

extern fun foo ():<> void
implement foo () = ()

The behavior seems inconsistent.

The ‘inconsistency’ is by design, though.

My recommended style for programming in ATS is that
‘implement’ should be used to implement non-recursive functions.

implement foo () = let
fun foo2 (…): void = … // foo2 is recursive
in
foo2 (…)
endOn Monday, December 16, 2013 11:48:19 AM UTC-5, Jyun-Yan You wrote:

There is a function.

fun foo ():<> void

If I mix declaration and definition in dats, the compiler complains about
missing termination metric.

fun foo ():<> void = ()

However, if I separate them, it compiles fine.

extern fun foo ():<> void
implement foo () = ()

The behavior seems inconsistent.