sorry case infects whole function?

Stream: lean4

[Yuri de Wit]

It seems that the interpreter does not evaluate a function containing a case with sorry even though the case being evaluated is implemented.

#mwe:

inductive Term
| val : Int -> Term
| add : Term -> Term -> Term
| sub : Term -> Term -> Term
| mul : Term -> Term -> Term
| div : Term -> Term -> Term
| if  : Term -> Term -> Term -> Term
deriving Repr

partial def reduce : Term -> Term
| v@(.val _)  => v
| .add l r    => goAdd (reduce l) (reduce r)
| .mul l r    => goMul (reduce l) (reduce r)
| .sub l r    => goSub (reduce l) (reduce r)
| .div l r    => goDiv (reduce l) (reduce r)
| .if c t e   => goIf  (reduce c) t e
where
  goAdd : Term -> Term -> Term
  | .val l, .val r => .val (l + r)
  | _, _ => sorry

  goSub : Term -> Term -> Term
  | .val l, .val r => .val (l - r)
  | _, _ => sorry

  goMul : Term -> Term -> Term
  | .val l, .val r => .val (l * r)
  | _, _ => sorry

  goDiv : Term -> Term -> Term
  | .val l, .val r => .val (l / r)
  | _, _ => sorry

  goIf : Term -> Term -> Term -> Term
  | .val n, t, e => if n > 0 then (reduce t) else (reduce e)
  | _, _, _ => sorry

#eval reduce (Term.val 2) -- cannot evaluate code because 'reduce.goAdd' uses 'sorry' and/or contains errors

Is this as designed or a TODO?

[Andrés Goens]

If you compile it it will run though

[Andrés Goens]

def main : IO Unit :=
  IO.println s!"{repr $ reduce (Term.val 2 )}"

will happily print "Term.val 2"