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.
