Zulip Chat Archive

Stream: new members

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


Chris M (Jul 29 2020 at 03:54):

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 (Jul 29 2020 at 04:00):

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 (Jul 29 2020 at 04:01):

Great, thanks!


Last updated: Dec 20 2023 at 11:08 UTC