How does the compiler deal with `if ... then .... else`

Stream: new members

[Chris M]

Is the if ... then .... else pattern in Lean a primitive pattern, or is it translated to something else somehow before the kernel deals with it? And what type of object is it? afaik, it's not part of simple lambda calculus. TPIL and the reference manual don't seem to answer my question.
E.g. I'm curious how the compiler deals with if h : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma h) y + 1 else zero in the following code:

open nat

def div_rec_lemma {x y : ℕ} : 0 < y ∧ y ≤ x → x - y < x :=
λ h, sub_lt (lt_of_lt_of_le h.left h.right) h.left

def div.F (x : ℕ) (f : Π x₁, x₁ < x → ℕ → ℕ) (y : ℕ) : ℕ :=
if h : 0 < y ∧ y ≤ x then
  f (x - y) (div_rec_lemma h) y + 1
else
  zero

def div := well_founded.fix lt_wf div.F

[Bryan Gin-ge Chen]

if ... then ... else is notation for either ite or dite, which are both functions defined on p : Prop with a decidable p type class. See 10.5 of TPiL.

[Chris M]

Great, thanks!