Termetric not well-founded

5 views
Skip to first unread message

David Smith

unread,
May 20, 2021, 5:16:28 PM5/20/21
to ats-lang-users
I'm having a bit of trouble to get anything with termination checking to run.

I produced a rather simple example:

implement
main0() =
  let
    fun
    fact{n:int} .<n>.
      (n: int(n)) : int =
        if n > 0
        then n * fact(n-1)
        else 1
  in println!("fact(5) = ", fact(5)) end

However when compiling this I get `unresolved constraint for termetric being well-founded:
C3NSTRprop(C3TKtermet_isnat(); S2Eapp(S2Ecst(gte_int_int); S2Evar(n(4282)), S2Eint(0)))`.

Can anyone help me figure out what I'm doing wrong?

David Smith

unread,
May 20, 2021, 5:25:40 PM5/20/21
to ats-lang-users
Oh, it works with n:nat. Epic!
Reply all
Reply to author
Forward
0 new messages