Two Types of Inling?

Stream: lean4

[Mac]

What is the difference between @[inline] and @[macroInline]?

[Leonardo de Moura]

[inline] respects Lean calling convention: call-by-value, [macroInline] is just delta+beta reduction.
Example:

def f (x y : Nat) := if x > 0 then y else 0

def g (a : Nat) := f a (fib (a + 1000))

If f is marked as [inline], g becomes

let x := a
let y := fib (a + 1000)
if x > 0 then y else 0

If f is marked as [macroInline], we have

if a > 0 then fib (a + 1000) else 0

[Leonardo de Moura]

We use [macroInline] in definitions such as

@[macroInline] def or (x y : Bool) : Bool :=
  match x with
  | true  => true
  | false => y

to make sure we get the behavior most users expect: y is not evaluated if x evaluates to true.

[Mac]

Thanks!