First, tri_test(0) is just: [un:int | 0 <= un; un+1 <= 0; un == 0; 0 == 0] int(un)
Clearly, no value can be given the above type as 0 <= un and un+1 <= 0 yields a contradiction. On Wed, Jun 30, 2021 at 10:12 PM d4v3y_5c0n3s <tmj9...@gmail.com> wrote: > So, I'm trying to get the following code to work: > *typedef tri_test2(v:int) = [un:int | 0 <= un; un+1 <= v; un == 0; v == 0] > int(un)* > *val test2 = (0):tri_test2(0)* > But I get the following error: > */tmp/patsopt_tcats_TCES3d: 196(line=6, offs=14) -- 197(line=6, offs=15): > error(3): unsolved constraint: C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(<=); > S2Eapp(S2Ecst(+); S2EVar(0->S2Eintinf(0)), S2Eintinf(1)), S2Eintinf(0)))* > *typechecking has failed: there are some unsolved constraints: please > inspect the above reported error message(s) for information.* > *exit(ATS): uncaught exception: > _2home_2hwxi_2Research_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)* > I am clueless as to why I keep getting this error. What is ATS having > trouble understanding here? > > -- > 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 ats-lang-users+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/ats-lang-users/3e48e488-e255-46d0-b6b7-3bab7fb538ban%40googlegroups.com > <https://groups.google.com/d/msgid/ats-lang-users/3e48e488-e255-46d0-b6b7-3bab7fb538ban%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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 ats-lang-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrM4pQ4CrVFgjs4M1m6PAiqJL_XOu%2BwyfY3T%2BNszWyReA%40mail.gmail.com.
