`[inline]` だと短絡評価できるのに `[always_inline]` だとできないという例

なんでやねん

@[inline]
def Bool.And₁ : Bool → Bool → Bool
  | true, true => true
  | _, _ => false

-- short circuiting!!
/-- info: false -/
#guard_msgs in
  #eval Bool.And₁ false (dbg_trace "hello"; true)

@[always_inline]
def Bool.And₂ : Bool → Bool → Bool
  | true, true => true
  | _, _ => false

-- **not** short circuiting!!
/--
info: hello
---
info: false
-/
#guard_msgs in
  #eval Bool.And₂ false (dbg_trace "hello"; true)

Start with the inline and always_inline definitions and their accompanying #guard_msgs examples in the issue body. Reproduce both evaluations, compare the emitted messages, and determine what explains the differing short-circuit behavior; done means the behavior is understood and the issue has a clear conclusion.