chore(frontends/lean): Π ==> ∀

src/frontends/lean/builtin_exprs.cpp

@@ -823,7 +823,7 @@ parse_table init_nud_table() {
     // r = r.add({transition("(:", Expr), transition(":)", mk_ext_action(parse_pattern))}, x0);
     r = r.add({transition("()", mk_ext_action(parse_unit))}, x0);
     r = r.add({transition("fun", mk_ext_action(parse_lambda))}, x0);
-    r = r.add({transition("Pi", Binders), transition(",", mk_scoped_expr_action(x0, 0, false))}, x0);
+    r = r.add({transition("forall", Binders), transition(",", mk_scoped_expr_action(x0, 0, false))}, x0);
     r = r.add({transition("Type", mk_ext_action(parse_Type))}, x0);
     r = r.add({transition("Type*", mk_ext_action(parse_Type_star))}, x0);
     r = r.add({transition("Sort", mk_ext_action(parse_Sort))}, x0);

src/frontends/lean/token_table.cpp

@@ -77,7 +77,7 @@ void for_each(token_table const & s, std::function<void(char const *, token_info
 
 void init_token_table(token_table & t) {
     pair<char const *, unsigned> builtin[] =
-        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"at", 0},
+        {{"fun", 0}, {"forall", 0}, {"let", 0}, {"in", 0}, {"at", 0},
          {"have", 0}, {"assume", 0}, {"show", 0}, {"suffices", 0},
          {"do", 0}, {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0},
          {"hiding", 0}, {"replacing", 0}, {"renaming", 0},
@@ -111,8 +111,7 @@ void init_token_table(token_table & t) {
          "#compile", "#unify", "#compact_tst", nullptr};
 
     pair<char const *, char const *> aliases[] =
-        {{"λ", "fun"}, {"forall", "Pi"},
-         {"∀", "Pi"}, {"Π", "Pi"}, {"(|", "⟨"}, {"|)", "⟩"}, {nullptr, nullptr}};
+        {{"λ", "fun"}, {"∀", "forall"}, {"(|", "⟨"}, {"|)", "⟩"}, {nullptr, nullptr}};
 
     pair<char const *, char const *> cmd_aliases[] =
         {{nullptr, nullptr}};

tests/bench/rbmap3.lean

@@ -34,19 +34,19 @@ protected def max : Rbnode α β → Option (Sigma (fun k => β k))
 | (Node _ _ k v leaf)   := some ⟨k, v⟩
 | (Node _ _ k v r)      := max r
 
-@[specialize] def fold (f : Π (k : α), β k → σ → σ) : Rbnode α β → σ → σ
+@[specialize] def fold (f : ∀ (k : α), β k → σ → σ) : Rbnode α β → σ → σ
 | leaf b               := b
 | (Node _ l k v r)   b := fold r (f k v (fold l b))
 
-@[specialize] def revFold (f : Π (k : α), β k → σ → σ) : Rbnode α β → σ → σ
+@[specialize] def revFold (f : ∀ (k : α), β k → σ → σ) : Rbnode α β → σ → σ
 | leaf b               := b
 | (Node _ l k v r)   b := revFold l (f k v (revFold r b))
 
-@[specialize] def all (p : Π k : α, β k → Bool) : Rbnode α β → Bool
+@[specialize] def all (p : ∀ k : α, β k → Bool) : Rbnode α β → Bool
 | leaf                 := true
 | (Node _ l k v r)     := p k v && all l && all r
 
-@[specialize] def any (p : Π k : α, β k → Bool) : Rbnode α β → Bool
+@[specialize] def any (p : ∀ k : α, β k → Bool) : Rbnode α β → Bool
 | leaf               := false
 | (Node _ l k v r)   := p k v || any l || any r
 
@@ -54,7 +54,7 @@ def isRed : Rbnode α β → Bool
 | (Node red _ _ _ _) := true
 | _                  := false
 
-def rotateLeft : Π (n : Rbnode α β), n ≠ leaf → Rbnode α β
+def rotateLeft : ∀ (n : Rbnode α β), n ≠ leaf → Rbnode α β
 | n@(Node hc hl hk hv (Node red xl xk xv xr)) _ :=
   if !isRed hl
   then (Node hc (Node red hl hk hv xl) xk xv xr)
@@ -74,7 +74,7 @@ theorem rotateLeftNeLeaf : ∀ (n : Rbnode α β) (h : n ≠ leaf), rotateLeft n
 | leaf h _                                := absurd rfl h
 | (Node _ _ _ _ (Node black _ _ _ _)) _ h := Rbnode.noConfusion h
 
-def rotateRight : Π (n : Rbnode α β), n ≠ leaf → Rbnode α β
+def rotateRight : ∀ (n : Rbnode α β), n ≠ leaf → Rbnode α β
 | n@(Node hc (Node red xl xk xv xr) hk hv hr) _ :=
   if isRed xl
   then (Node hc xl xk xv (Node red xr hk hv hr))
@@ -95,7 +95,7 @@ def flipColor : Rbnode α β → Rbnode α β
 | (Node c l k v r) := Node (flip c) l k v r
 | leaf             := leaf
 
-def flipColors : Π (n : Rbnode α β), n ≠ leaf → Rbnode α β
+def flipColors : ∀ (n : Rbnode α β), n ≠ leaf → Rbnode α β
 | n@(Node c l k v r) _ :=
   if isRed l ∧ isRed r
   then Node (flip c) (flipColor l) k v (flipColor r)
@@ -133,7 +133,7 @@ variable (lt : α → α → Prop)
 
 variable [DecidableRel lt]
 
-def findCore : Rbnode α β → Π k : α, Option (Sigma (fun k => β k))
+def findCore : Rbnode α β → ∀ k : α, Option (Sigma (fun k => β k))
 | leaf                 x := none
 | (Node _ a ky vy b) x :=
   (match cmpUsing lt x ky with

tests/lean/run/csimp_type_error.lean

@@ -8,10 +8,10 @@ open type
 def value : type -> Type
   | (bv w) := {n // n < w}
 
-def tester_fails : Π {tp : type}, value tp -> Bool
+def tester_fails : ∀ {tp : type}, value tp -> Bool
   | (bv _) v1 := decide (v1.val = 0)
 
-def tester_ok : Π{tp : type}, value tp -> Prop
+def tester_ok : ∀ {tp : type}, value tp -> Prop
   | (bv _) v1 := v1.val = 0
 
 end scratch

tests/lean/run/new_compiler.lean

@@ -61,8 +61,8 @@ def bla' (i : Nat) (h : i > 0 ∧ i ≠ 10) : Nat :=
 
 inductive vec (α : Type u) : Nat → Type u
 | nil {}  : vec 0
-| cons    : Π {n}, α → vec n → vec (Nat.succ n)
+| cons    : ∀ {n}, α → vec n → vec (Nat.succ n)
 
-def vec.map {α β σ : Type u} (f : α → β → σ) : Π {n : Nat}, vec α n → vec β n → vec σ n
+def vec.map {α β σ : Type u} (f : α → β → σ) : ∀ {n : Nat}, vec α n → vec β n → vec σ n
 | _ vec.nil vec.nil                 := vec.nil
 | _ (vec.cons a as) (vec.cons b bs) := vec.cons (f a b) (vec.map as bs)

tests/lean/run/noncomputable_bug.lean

@@ -1,4 +1,4 @@
-axiom f : Π A : Type, A → Type
+axiom f : ∀ A : Type, A → Type
 
-def ex5b (α : Type) (a : α) : Π A : Type, A → Type :=
+def ex5b (α : Type) (a : α) : ∀ A : Type, A → Type :=
 f

tests/lean/trust0/basic.lean

@@ -12,7 +12,7 @@ namespace Nat
 
 inductive lessThanOrEqual (a : ℕ) : ℕ → Prop
 | refl : lessThanOrEqual a
-| step : Π {b}, lessThanOrEqual b → lessThanOrEqual (succ b)
+| step : ∀ {b}, lessThanOrEqual b → lessThanOrEqual (succ b)
 
 @[elabAsEliminator]
 theorem lessThanOrEqual.ndrec  {a : Nat} {C : Nat → Prop} (m₁ : C a) (m₂ : ∀ (b : Nat), lessThanOrEqual a b → C b → C (succ b)) {b : ℕ} (h : lessThanOrEqual a b) : C b :=
@@ -52,7 +52,7 @@ instance : HasSub ℕ :=
 instance : HasMul ℕ :=
 ⟨Nat.mul⟩
 
-def hasDecEq : Π a b : Nat, Decidable (a = b)
+def hasDecEq : ∀ (a b : Nat), Decidable (a = b)
 | zero     zero     := isTrue rfl
 | (succ x) zero     := isFalse (fun h => Nat.noConfusion h)
 | zero     (succ y) := isFalse (fun h => Nat.noConfusion h)