Oh, it works with n:nat. Epic!
David Smith schrieb am Donnerstag, 20. Mai 2021 um 21:16:28 UTC:
> 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?
>
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/f093aa00-f165-42f0-866e-e266ad627fcfn%40googlegroups.com.
