Lazy evaluation in Option.orElse?

Stream: lean4

[Siddhartha Gadgil]

In scala the argument to orElse for an Option is "call by name", so will not get evaluated if the first entry is not empty. Is this the case in lean 4 (did not look that way)? Alternatively, can I assume that evaluation is not done till a pattern is matched? Or should I explicitly use a Thunk?

Thanks.

[Mario Carneiro]

You should generally assume that arguments to a function will be evaluated eagerly unless they appear inside a function (either a thunk or a proof argument like in Decidable)

[Mario Carneiro]

There are some exceptions to this when the functions in question are inlined

[Siddhartha Gadgil]

Thanks. Then I will try to work with thunks.

[Mario Carneiro]

@Siddhartha Gadgil I just tested Option.orElse, and it does appear to be one of the exceptions. You can use dbgTrace to check whether a subterm is evaluated:

#eval Option.orElse (some 1) (dbgTrace "foo" fun _ => none) -- no output
#eval Option.orElse none (dbgTrace "foo" fun _ => some 1) -- foo

[Mario Carneiro]

It is marked @[macroInline], presumably because inlining it is relevant to evaluation order

[Siddhartha Gadgil]

Thanks a lot. That makes life more pleasant.