BinderInfo and reduction

Stream: lean4

[Arthur Paulino]

Is BinderInfo used for reductions of expressions?

[Gabriel Ebner]

Yes and no. In most cases they're ignored. Even alpha-equality does not care about the binder info:

import Lean
open Lean
#eval mkLambda `a BinderInfo.default  (mkSort levelOne) (mkBVar 0)
   == mkLambda `a BinderInfo.implicit (mkSort levelOne) (mkBVar 0)
-- true

[Gabriel Ebner]

There is one corner case, namely that the binder info in definitions can determine how hard Lean tries to reduce arguments:

def Nat' := Nat

-- fails
def f (α : Type) := α
example : f Nat = f Nat' := by with_reducible rfl

-- succeeds
def g {α : Type} := α
example : g (α := Nat) = g (α := Nat') := by with_reducible rfl

[Gabriel Ebner]

The only difference between the two examples is the binder info of the first argument of f/g. The with_reducible tells Lean to only unfold definitions that are marked reducible. But if the argument is implicit, then Lean tries harder and unfolds non-reducible definitions (Nat') as well.