Please use ifcase-expressions: fun foo {n:int} (n:int(n)): void = ifcase | n = 0 => () where {prval () = prop_verify{n == 0}()} | n = 1 => () where {prval () = prop_verify{n == 1}()} | _ (*else*) => () where {prval () = prop_verify{n != 0 && n != 1}()}
###### Also, you can use '+' and '*' for || and &&, respectively. For instance, if a <= 5 * b <= 5 then ... else ... And '+' and '*' have the types expected by you. On Sat, Jul 25, 2020 at 10:35 PM Dambaev Alexander <ice.redm...@gmail.com> wrote: > Hi, > > We know, that ATS is able to keep information about check in appropriate > branch of 'if' expression, like: > > ``` > fn foo( i: int): int = > if i < 1 > then (* here typechecker knows, that i < 1*) > else (* here typechecker knows, that i >= 1*) > ``` > > But sometimes, you need to use more conditions and case expressions is > more convenient in this case, but currently, typechecker is not always able > to keep such info in branches of 'case', like: > > ``` > fn foo( a: int, b: int): int = > case+ 0 of > | _ when a > 10 => ... > | _ when a > 5 => ... > | _ when b > 10 => ... > | _ when b > 5 => ... > | _ => (* 1 *) > ``` > > It will be great, if, at least in ATS3, at mark 1 typechecker will know, > that a <= 5 and b <= 5, because currently, as far as I got, condition like: > ``` > if a <= 5 && b <= 5 > then (* 1 *) > else (* 2 *) > ``` > will tell typechecker, that there is a proof 'a <= 5 && b <= 5', but there > are no separate proofs 'a <= 5' and 'b<=5' so you have to make a nested > if-expressions to get them, which is not so compact as 'case' expressions > > -- > 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/CAHjn2KxS8iGdxHRjVU2MJu_%2B5g143Lq6HKFo%2BRta06aF3ENdgg%40mail.gmail.com > <https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KxS8iGdxHRjVU2MJu_%2B5g143Lq6HKFo%2BRta06aF3ENdgg%40mail.gmail.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/CAPPSPLoAtWmL0kRe1Hpd5P%3DPMazOkzg5VeZr2pVAn%2B%3D%3DF2teEQ%40mail.gmail.com.