Why doesn't this get reduced?

Stream: new members

[Etienne Marion]

Why is the following expression not reduced?

#reduce (fun (f : Nat → Nat) ↦ ∀ (n : Nat), f n = f (n + 1)) Nat.succ

It appears in Metaprogramming in Lean 4 But there it says it should reduce to

∀ (n : Nat), Nat.succ n = Nat.succ (Nat.succ n)

which it doesn't.

[Aaron Liu]

I think you have to #reduce (types := true)

[Etienne Marion]

Indeed that works, but why?

[Aaron Liu]

because (fun (f : Nat → Nat) ↦ ∀ (n : Nat), f n = f (n + 1)) Nat.succ is a type?

[Etienne Marion]

Obviously :man_facepalming: thanks!