If conditions and constrains

Google Group
1

‘&&’ is a macro (due to shortcut evaluation); it is not given a dependent
type.

Replacing ‘&&’ with * (bmul) should work, though.On Thursday, April 10, 2014 8:50:37 PM UTC-4, Chris Double wrote:

The following code typechecks:

extern fun foo {n:nat | n > 50} (x: int n): void

implement main(): int =
let
val b = 20;
val c = 10;
val () = if c > 50 then foo (c) else ()
in
0
end

But this does not:

extern fun foo {n:nat | n > 50} (x: int n): void

implement main(): int =
let
val b = 20;
val c = 10;
val () = if c > 50 && b > 10 then foo (c) else ()
in
0
end

Why does adding another condition in the ‘if’, which doesn’t change
the logic since ‘c’ is not greater than 50, cause a constraint error.
The constraint seems to be that 10 is not greater than 50.

Breaking the condition out does typecheck:

extern fun foo {n:nat | n > 50} (x: int n): void

implement main(): int =
let
val b = 20;
val c = 10;
val () = if c > 50 then
if b > 10 then foo (c)
else ()
else ()
in
0
end

–
http://www.bluishcoder.co.nz