Diverging match statement

Stream: new members

[Michael Rothgang]

Is there a way in Lean to write a divergent match? Something like (code doesn't work):

def main : Nat :=
  -- Simplified; real code is a longer computation.
  let n : Option Nat := some 42
  -- My goal: handle the "error case" by exiting the function directly,
  -- and work with the inner value instead. How can I do this?
  let nreal := match n with
   | some n => n
   | none => return 2
  return nreal

[Patrick Massot]

I’m not sure what you are trying to do, I suspect there are typos in your snippet.

[Damiano Testa]

Is

  if h : n.isSome then
    let nreal := n.get h
    nreal
  else
    0  -- what should the function return here?

not good?

[Patrick Massot]

First, do you really want this to be main? This would need to be a IO program. Or did you pick the name main at random?

[Patrick Massot]

And was your last line meant to be return nreal?

[Patrick Massot]

If my interpretation is correct then you can use the Id monad to do that.

[Patrick Massot]

Something like:

def foo : Nat := Id.run do
  -- Simplified; real code is a longer computation.
  let n : Option Nat := some 42
  -- My goal: handle the "error case" by exiting the function directly,
  -- and work with the inner value instead. How can I do this?
  let nreal ← match n with
   | some n => n
   | none => return 2
  return nreal

[Damiano Testa]

and, in Patrick's code, you can also shorten the match to let some nreal := n | return 2.

[Patrick Massot]

Maybe the example is clearer if you write

def foo (n : Option Nat) : Nat := Id.run do
  -- My goal: handle the "error case" by exiting the function directly,
  -- and work with the inner value instead. How can I do this?
  let nreal ← match n with
   | some n => n
   | none => return 2
  let nreal := nreal + 1
  return nreal

This way you can use #eval foo (some 4) and #eval foo none to convince yourself that the let nreal := nreal + 1 is not executed in the second example.