涉及andalso宏ATS

Question

类型检查错误这里有两段代码我认为是等价的除了具有更多的行，那么它应该在第二个：

fun 
move_ul 
{i:nat} 
(
    p: int(i) 
, ms: list0(Int) 
): list0(Int) = 
if p - 5 >= 0 andalso p % 4 != 0 then 
    move_ul(p - 5, cons0(p - 5, ms)) 
else 
    ms 



fun 
move_ul 
{i:nat} 
(
    p: int(i) 
, ms: list0(Int) 
): list0(Int) = 
if p % 4 != 0 then 
    if p - 5 >= 0 then 
    move_ul(p - 5, cons0(p - 5, ms)) 
    else 
    ms 
else 
    ms 

出于某种原因，第二个存活类型检查和第一个没有（不满足约束条件）......有人能告诉我为什么吗？

Answer 1

这是由于定义了andalso的方式（作为不使用依赖类型的宏）。如果将andalso更改为*（它重载布尔乘法），则应该检查代码的第一个版本。

顺便说一句，如果使用orelse，类似的情况可以简单地通过orelse替换+（它重载布尔加法）来解决。