小编Dar*_*ley的帖子

这里有两段代码我认为是等效的，除了第二段的行数比它应该多：

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

出于某种原因，第二个在类型检查中幸存下来，第一个没有（未能满足约束）......有人能告诉我为什么吗？