Pi token?

Stream: lean4

[Ryan Lahfa]

Hi there, I might have a stupid question but why the Pi syntax does not work?

import Mathlib.Tactic.Basic

universe u

theorem monotonicity.pi {α: Sort u} {p q : α -> Prop} (h: ∀a, p a -> q a):
  (Πa, p a) -> (Πa, q a) := sorry

It's failing with unexpected token at the first Pi

(I'm trying my hand at porting the coinductives predicates)

Grepping Lean 4 source code seems to say that Pi behaves like a binder, right?

[Daniel Fabian]

Lean 4 uniformly uses the forall syntax instead of pi for types and forall for propositions

[Sebastian Ullrich]

That is not quite correct. In Type, we usually use the Agda-like (a : A) -> B a, which is also closer to the (a : A) : B a syntax in declaration headers.

[Max]

https://leanprover.github.io/lean4/doc/lean3changes.html#dependent-function-types This may be informative for you.

[Max]

(And https://leanprover.github.io/lean4/doc/lean3changes.html#lambda-expressions to a lesser degree as well I guess)