refactor(frontends/lean): replace '[protected]' modifier with 'protected definition' and 'protected theorem', '[protected]' is not a hint.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

library/data/bool.lean

@@ -10,10 +10,10 @@ inductive bool : Type :=
   ff : bool,
   tt : bool
 namespace bool
-  definition rec_on [protected] {C : bool → Type} (b : bool) (H₁ : C ff) (H₂ : C tt) : C b :=
+  protected definition rec_on {C : bool → Type} (b : bool) (H₁ : C ff) (H₂ : C tt) : C b :=
   rec H₁ H₂ b
 
-  definition cases_on [protected] {p : bool → Prop} (b : bool) (H₁ : p ff) (H₂ : p tt) : p b :=
+  protected definition cases_on {p : bool → Prop} (b : bool) (H₁ : p ff) (H₂ : p tt) : p b :=
   rec H₁ H₂ b
 
   definition cond {A : Type} (b : bool) (t e : A) :=
@@ -135,10 +135,10 @@ namespace bool
   theorem bnot_true  : !tt = ff :=
   rfl
 
-  theorem is_inhabited [protected] [instance] : inhabited bool :=
+  protected theorem is_inhabited [instance] : inhabited bool :=
   inhabited.mk ff
 
-  theorem has_decidable_eq [protected] [instance] : decidable_eq bool :=
+  protected theorem has_decidable_eq [instance] : decidable_eq bool :=
   take a b : bool,
     rec_on a
       (rec_on b (inl rfl) (inr ff_ne_tt))

library/data/empty.lean

@@ -10,7 +10,7 @@ import logic.core.cast
 inductive empty : Type
 
 namespace empty
-  theorem elim [protected] (A : Type) (H : empty) : A :=
+  protected theorem elim (A : Type) (H : empty) : A :=
   rec (λe, A) H
 end empty
 

library/data/int/basic.lean

@@ -184,7 +184,7 @@ representative_map_idempotent_equiv proj_rel @proj_congr a
 
 -- ## Definition of ℤ and basic theorems and definitions
 
-opaque definition int [protected] := image proj
+protected opaque definition int := image proj
 notation `ℤ` := int
 
 opaque definition psub : ℕ × ℕ → ℤ := fun_image proj
@@ -203,7 +203,7 @@ exists_intro (pr1 (rep a))
       a = psub (rep a) : (psub_rep a)⁻¹
     ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod_ext (rep a))⁻¹}))
 
-theorem has_decidable_eq [instance] [protected] : decidable_eq ℤ :=
+protected theorem has_decidable_eq [instance] : decidable_eq ℤ :=
 take a b : ℤ, _
 
 reducible [off] int

library/data/list/basic.lean

@@ -29,15 +29,15 @@ section
 
 variable {T : Type}
 
-theorem induction_on [protected] {P : list T → Prop} (l : list T) (Hnil : P nil)
+protected theorem induction_on {P : list T → Prop} (l : list T) (Hnil : P nil)
     (Hind : ∀ (x : T) (l : list T),  P l → P (x::l)) : P l :=
 rec Hnil Hind l
 
-theorem cases_on [protected] {P : list T → Prop} (l : list T) (Hnil : P nil)
+protected theorem cases_on {P : list T → Prop} (l : list T) (Hnil : P nil)
     (Hcons : ∀ (x : T) (l : list T), P (x::l)) : P l :=
 induction_on l Hnil (take x l IH, Hcons x l)
 
-definition rec_on [protected] {A : Type} {C : list A → Type} (l : list A)
+protected definition rec_on {A : Type} {C : list A → Type} (l : list A)
     (H1 : C nil) (H2 : Π (h : A) (t : list A), C t → C (h::t)) : C l :=
   rec H1 H2 l
 

library/data/nat/basic.lean

@@ -30,14 +30,14 @@ theorem rec_zero {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m))
 theorem rec_succ {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) (n : ℕ) :
   nat.rec x f (succ n) = f n (nat.rec x f n)
 
-theorem induction_on [protected] {P : ℕ → Prop} (a : ℕ) (H1 : P zero) (H2 : ∀ (n : ℕ) (IH : P n), P (succ n)) :
+protected theorem induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P zero) (H2 : ∀ (n : ℕ) (IH : P n), P (succ n)) :
   P a :=
 nat.rec H1 H2 a
 
-definition rec_on [protected] {P : ℕ → Type} (n : ℕ) (H1 : P zero) (H2 : ∀m, P m → P (succ m)) : P n :=
+protected definition rec_on {P : ℕ → Type} (n : ℕ) (H1 : P zero) (H2 : ∀m, P m → P (succ m)) : P n :=
 nat.rec H1 H2 n
 
-theorem is_inhabited [protected] [instance] : inhabited nat :=
+protected theorem is_inhabited [instance] : inhabited nat :=
 inhabited.mk zero
 
 -- Coercion from num
@@ -105,7 +105,7 @@ induction_on n
     absurd H ne)
   (take k IH H, IH (succ_inj H))
 
-theorem has_decidable_eq [instance] [protected] : decidable_eq ℕ :=
+protected theorem has_decidable_eq [instance] : decidable_eq ℕ :=
 take n m : ℕ,
 have general : ∀n, decidable (n = m), from
   rec_on m

library/data/nat/order.lean

@@ -430,7 +430,7 @@ theorem ge_decidable [instance] (n m : ℕ) : decidable (n ≥ m)
 
 -- ### misc
 
-theorem strong_induction_on [protected] {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n :=
+protected theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n :=
 have H1 : ∀ {n m : nat}, m < n → P m, from
   take n,
   induction_on n
@@ -446,7 +446,7 @@ have H1 : ∀ {n m : nat}, m < n → P m, from
           (assume H4: m = n', H4⁻¹ ▸ H2)),
 H1 self_lt_succ
 
-theorem case_strong_induction_on [protected] {P : nat → Prop} (a : nat) (H0 : P 0)
+protected theorem case_strong_induction_on {P : nat → Prop} (a : nat) (H0 : P 0)
   (Hind : ∀(n : nat), (∀m, m ≤ n → P m) → P (succ n)) : P a :=
 strong_induction_on a (
   take n,

library/data/num.lean

@@ -18,11 +18,11 @@ theorem pos_num.is_inhabited [instance] : inhabited pos_num :=
 inhabited.mk pos_num.one
 
 namespace pos_num
-  theorem induction_on [protected] {P : pos_num → Prop} (a : pos_num)
+  protected theorem induction_on {P : pos_num → Prop} (a : pos_num)
       (H₁ : P one) (H₂ : ∀ (n : pos_num), P n → P (bit1 n)) (H₃ : ∀ (n : pos_num), P n → P (bit0 n)) : P a :=
   rec H₁ H₂ H₃ a
 
-  definition rec_on [protected] {P : pos_num → Type} (a : pos_num)
+  protected definition rec_on {P : pos_num → Type} (a : pos_num)
       (H₁ : P one) (H₂ : ∀ (n : pos_num), P n → P (bit1 n)) (H₃ : ∀ (n : pos_num), P n → P (bit0 n)) : P a :=
   rec H₁ H₂ H₃ a
 
@@ -125,11 +125,11 @@ inhabited.mk num.zero
 
 namespace num
   open pos_num
-  theorem induction_on [protected] {P : num → Prop} (a : num)
+  protected theorem induction_on {P : num → Prop} (a : num)
       (H₁ : P zero) (H₂ : ∀ (p : pos_num), P (pos p)) : P a :=
   rec H₁ H₂ a
 
-  definition rec_on [protected] {P : num → Type} (a : num)
+  protected definition rec_on {P : num → Type} (a : num)
       (H₁ : P zero) (H₂ : ∀ (p : pos_num), P (pos p)) : P a :=
   rec H₁ H₂ a
 

library/data/option.lean

@@ -10,11 +10,11 @@ inductive option (A : Type) : Type :=
   some    : A → option A
 
 namespace option
-  theorem induction_on [protected] {A : Type} {p : option A → Prop} (o : option A)
+  protected theorem induction_on {A : Type} {p : option A → Prop} (o : option A)
     (H1 : p none) (H2 : ∀a, p (some a)) : p o :=
   rec H1 H2 o
 
-  definition rec_on [protected] {A : Type} {C : option A → Type} (o : option A)
+  protected definition rec_on {A : Type} {C : option A → Type} (o : option A)
     (H1 : C none) (H2 : ∀a, C (some a)) : C o :=
   rec H1 H2 o
 
@@ -32,13 +32,13 @@ namespace option
     (H ▸ is_none_none)
     (not_is_none_some a)
 
-  theorem equal [protected] {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = a₂ :=
+  protected theorem equal {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = a₂ :=
   congr_arg (option.rec a₁ (λ a, a)) H
 
-  theorem is_inhabited [protected] [instance] (A : Type) : inhabited (option A) :=
+  protected theorem is_inhabited [instance] (A : Type) : inhabited (option A) :=
   inhabited.mk none
 
-  theorem has_decidable_eq [protected] [instance] {A : Type} (H : decidable_eq A) : decidable_eq (option A) :=
+  protected theorem has_decidable_eq [instance] {A : Type} (H : decidable_eq A) : decidable_eq (option A) :=
   take o₁ o₂ : option A,
     rec_on o₁
       (rec_on o₂ (inl rfl) (take a₂, (inr (none_ne_some a₂))))

library/data/prod.lean

@@ -31,7 +31,7 @@ section
   theorem pr2_pair (a : A) (b : B) : pr2 (a, b) = b :=
   rfl
 
-  theorem destruct [protected] {P : A × B → Prop} (p : A × B) (H : ∀a b, P (a, b)) : P p :=
+  protected theorem destruct {P : A × B → Prop} (p : A × B) (H : ∀a b, P (a, b)) : P p :=
   rec H p
 
   theorem prod_ext (p : prod A B) : pair (pr1 p) (pr2 p) = p :=
@@ -42,13 +42,13 @@ section
   theorem pair_eq {a1 a2 : A} {b1 b2 : B} (H1 : a1 = a2) (H2 : b1 = b2) : (a1, b1) = (a2, b2) :=
   H1 ▸ H2 ▸ rfl
 
-  theorem equal [protected] {p1 p2 : prod A B} : ∀ (H1 : pr1 p1 = pr1 p2) (H2 : pr2 p1 = pr2 p2), p1 = p2 :=
+  protected theorem equal {p1 p2 : prod A B} : ∀ (H1 : pr1 p1 = pr1 p2) (H2 : pr2 p1 = pr2 p2), p1 = p2 :=
   destruct p1 (take a1 b1, destruct p2 (take a2 b2 H1 H2, pair_eq H1 H2))
 
-  theorem is_inhabited [protected] [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
+  protected theorem is_inhabited [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
   inhabited.destruct H1 (λa, inhabited.destruct H2 (λb, inhabited.mk (pair a b)))
 
-  theorem has_decidable_eq [protected] [instance] (H1 : decidable_eq A) (H2 : decidable_eq B) : decidable_eq (A × B) :=
+  protected theorem has_decidable_eq [instance] (H1 : decidable_eq A) (H2 : decidable_eq B) : decidable_eq (A × B) :=
   take u v : A × B,
     have H3 : u = v ↔ (pr1 u = pr1 v) ∧ (pr2 u = pr2 v), from
       iff.intro

library/data/sigma.lean

@@ -19,7 +19,7 @@ section
   theorem dpr1_dpair (a : A) (b : B a) : dpr1 (dpair a b) = a := rfl
   theorem dpr2_dpair (a : A) (b : B a) : dpr2 (dpair a b) = b := rfl
 
-  theorem destruct [protected] {P : sigma B → Prop} (p : sigma B) (H : ∀a b, P (dpair a b)) : P p :=
+  protected theorem destruct {P : sigma B → Prop} (p : sigma B) (H : ∀a b, P (dpair a b)) : P p :=
   rec H p
 
   theorem dpair_ext (p : sigma B) : dpair (dpr1 p) (dpr2 p) = p :=
@@ -34,11 +34,11 @@ section
                 ... = dpair a₁ b₂                : {H₂})
     b₂ H₁ H₂
 
-  theorem equal [protected] {p₁ p₂ : Σx : A, B x} :
+  protected theorem equal {p₁ p₂ : Σx : A, B x} :
     ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : eq.rec_on H₁ (dpr2 p₁) = (dpr2 p₂)), p₁ = p₂ :=
   destruct p₁ (take a₁ b₁, destruct p₂ (take a₂ b₂ H₁ H₂, dpair_eq H₁ H₂))
 
-  theorem is_inhabited [protected] [instance] (H₁ : inhabited A) (H₂ : inhabited (B (default A))) :
+  protected theorem is_inhabited [instance] (H₁ : inhabited A) (H₂ : inhabited (B (default A))) :
     inhabited (sigma B) :=
   inhabited.destruct H₁ (λa, inhabited.destruct H₂ (λb, inhabited.mk (dpair (default A) b)))
 end

library/data/string.lean

@@ -10,7 +10,7 @@ inductive char : Type :=
   mk : bool → bool → bool → bool → bool → bool → bool → bool → char
 
 namespace char
-  theorem is_inhabited [protected] [instance] : inhabited char :=
+  protected theorem is_inhabited [instance] : inhabited char :=
   inhabited.mk (mk ff ff ff ff ff ff ff ff)
 end char
 
@@ -19,6 +19,6 @@ inductive string : Type :=
   str   : char → string → string
 
 namespace string
-  theorem is_inhabited [protected] [instance] : inhabited string :=
+  protected theorem is_inhabited [instance] : inhabited string :=
   inhabited.mk empty
 end string

library/data/subtype.lean

@@ -22,7 +22,7 @@ section
 
   theorem elt_of_tag (a : A) (H : P a) : elt_of (tag a H) = a := rfl
 
-  theorem destruct [protected] {Q : {x, P x} → Prop} (a : {x, P x})
+  protected theorem destruct {Q : {x, P x} → Prop} (a : {x, P x})
       (H : ∀(x : A) (H1 : P x), Q (tag x H1)) : Q a :=
     rec H a
 
@@ -35,13 +35,13 @@ section
   theorem tag_eq {a1 a2 : A} {H1 : P a1} {H2 : P a2} (H3 : a1 = a2) : tag a1 H1 = tag a2 H2 :=
   eq.subst H3 (take H2, tag_irrelevant H1 H2) H2
 
-  theorem equal [protected] {a1 a2 : {x, P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 :=
+  protected theorem equal {a1 a2 : {x, P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 :=
   destruct a1 (take x1 H1, destruct a2 (take x2 H2 H, tag_eq H))
 
-  theorem is_inhabited [protected] [instance] {a : A} (H : P a) : inhabited {x, P x} :=
+  protected theorem is_inhabited [instance] {a : A} (H : P a) : inhabited {x, P x} :=
   inhabited.mk (tag a H)
 
-  theorem has_decidable_eq [protected] [instance] (H : decidable_eq A) : decidable_eq {x, P x} :=
+  protected theorem has_decidable_eq [instance] (H : decidable_eq A) : decidable_eq {x, P x} :=
   take a1 a2 : {x, P x},
     have H1 : (a1 = a2) ↔ (elt_of a1 = elt_of a2), from
       iff.intro (assume H, eq.subst H rfl) (assume H, equal H),

library/data/sum.lean

@@ -17,11 +17,11 @@ namespace sum
     infixr `+`:25 := sum    -- conflicts with notation for addition
   end extra_notation
 
-  definition rec_on [protected] {A B : Type} {C : (A ⊎ B) → Type} (s : A ⊎ B)
+  protected definition rec_on {A B : Type} {C : (A ⊎ B) → Type} (s : A ⊎ B)
     (H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s :=
   rec H1 H2 s
 
-  definition cases_on [protected] {A B : Type} {P : (A ⊎ B) → Prop} (s : A ⊎ B)
+  protected definition cases_on {A B : Type} {P : (A ⊎ B) → Prop} (s : A ⊎ B)
     (H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s :=
   rec H1 H2 s
 
@@ -49,13 +49,13 @@ namespace sum
   have H2 : f (inr A b2), from H ▸ H1,
   H2
 
-  theorem is_inhabited_left [protected] [instance] {A B : Type} (H : inhabited A) : inhabited (A ⊎ B) :=
+  protected theorem is_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A ⊎ B) :=
   inhabited.mk (inl B (default A))
 
-  theorem is_inhabited_right [protected] [instance] {A B : Type} (H : inhabited B) : inhabited (A ⊎ B) :=
+  protected theorem is_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabited (A ⊎ B) :=
   inhabited.mk (inr A (default B))
 
-  theorem has_eq_decidable [protected] [instance] {A B : Type} (H1 : decidable_eq A) (H2 : decidable_eq B) :
+  protected theorem has_eq_decidable [instance] {A B : Type} (H1 : decidable_eq A) (H2 : decidable_eq B) :
        decidable_eq (A ⊎ B) :=
   take s1 s2 : A ⊎ B,
     rec_on s1

library/data/unit.lean

@@ -9,15 +9,15 @@ inductive unit : Type :=
 namespace unit
   notation `⋆`:max := star
 
-  theorem equal [protected] (a b : unit) : a = b :=
+  protected theorem equal (a b : unit) : a = b :=
   rec (rec rfl b) a
 
   theorem eq_star (a : unit) : a = star :=
   equal a star
 
-  theorem is_inhabited [protected] [instance] : inhabited unit :=
+  protected theorem is_inhabited [instance] : inhabited unit :=
   inhabited.mk ⋆
 
-  theorem has_decidable_eq [protected] [instance] : decidable_eq unit :=
+  protected theorem has_decidable_eq [instance] : decidable_eq unit :=
   take (a b : unit), inl (equal a b)
 end unit

library/data/vector.lean

@@ -15,19 +15,19 @@ namespace vec
   section sc_vec
   variable {T : Type}
 
-  theorem rec_on [protected] {C : ∀ (n : ℕ), vec T n → Type} {n : ℕ} (v : vec T n) (Hnil : C 0 nil)
+  protected theorem rec_on {C : ∀ (n : ℕ), vec T n → Type} {n : ℕ} (v : vec T n) (Hnil : C 0 nil)
     (Hcons : ∀(x : T) {n : ℕ} (w : vec T n), C n w → C (succ n) (cons x w)) : C n v :=
   rec Hnil Hcons v
 
-  theorem induction_on [protected] {C : ∀ (n : ℕ), vec T n → Prop} {n : ℕ} (v : vec T n) (Hnil : C 0 nil)
+  protected theorem induction_on {C : ∀ (n : ℕ), vec T n → Prop} {n : ℕ} (v : vec T n) (Hnil : C 0 nil)
     (Hcons : ∀(x : T) {n : ℕ} (w : vec T n), C n w → C (succ n) (cons x w)) : C n v :=
   rec_on v Hnil Hcons
 
-  theorem case_on [protected] {C : ∀ (n : ℕ), vec T n → Type} {n : ℕ} (v : vec T n) (Hnil : C 0 nil)
+  protected theorem case_on {C : ∀ (n : ℕ), vec T n → Type} {n : ℕ} (v : vec T n) (Hnil : C 0 nil)
     (Hcons : ∀(x : T) {n : ℕ} (w : vec T n), C (succ n) (cons x w)) : C n v :=
   rec_on v Hnil (take x n v IH, Hcons x v)
 
-  theorem is_inhabited [instance] [protected] (A : Type) (H : inhabited A) (n : nat) : inhabited (vec A n) :=
+  protected theorem is_inhabited [instance] (A : Type) (H : inhabited A) (n : nat) : inhabited (vec A n) :=
   nat.rec_on n
     (inhabited.mk (@vec.nil A))
     (λ (n : nat) (iH : inhabited (vec A n)),

library/hott/path.lean

@@ -23,7 +23,7 @@ infix `≈` := path
 notation x `≈` y:50 `:>`:0 A:0 := @path A x y    -- TODO: is this right?
 definition idp {A : Type} {a : A} := idpath a
 
-definition induction_on [protected] {A : Type} {a b : A} (p : a ≈ b)
+protected definition induction_on {A : Type} {a b : A} (p : a ≈ b)
   {C : Π (b : A) (p : a ≈ b), Type} (H : C a (idpath a)) : C b p :=
 path.rec H p
 

library/logic/core/decidable.lean

@@ -16,10 +16,10 @@ inl trivial
 theorem false_decidable [instance] : decidable false :=
 inr not_false_trivial
 
-theorem induction_on [protected] {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
+protected theorem induction_on {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
 decidable.rec H1 H2 H
 
-definition rec_on [protected] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) :
+protected definition rec_on {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) :
   C :=
 decidable.rec H1 H2 H
 

library/logic/core/inhabited.lean

@@ -9,7 +9,7 @@ mk : A → inhabited A
 
 namespace inhabited
 
-definition destruct [protected] {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B :=
+protected definition destruct {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B :=
 inhabited.rec H2 H1
 
 definition Prop_inhabited [instance] : inhabited Prop :=

library/logic/core/nonempty.lean

@@ -8,7 +8,7 @@ inductive nonempty (A : Type) : Prop :=
 intro : A → nonempty A
 
 namespace nonempty
-  definition elim [protected] {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B :=
+  protected definition elim {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B :=
   rec H2 H1
 
   theorem inhabited_imp_nonempty [instance] {A : Type} (H : inhabited A) : nonempty A :=

src/emacs/lean-syntax.el

@@ -8,7 +8,7 @@
 (require 'rx)
 
 (defconst lean-keywords
-  '("import" "reducible" "tactic_hint" "private" "opaque" "definition" "renaming"
+  '("import" "reducible" "tactic_hint" "protected" "private" "opaque" "definition" "renaming"
     "inline" "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture"
     "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem"
     "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment"
@@ -70,8 +70,8 @@
      ;; place holder
      (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
      ;; modifiers
-     (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[protected\]"
+     (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]"
-               "\[instance\]" "\[class\]" "\[coercion\]" "\[off\]" "\[none\]" "\[on\]")) . 'font-lock-doc-face)
+               "\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]")) . 'font-lock-doc-face)
      ;; tactics
      (,(rx symbol-start
            (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "back" "beta" "done" "exact" "repeat")

src/frontends/lean/decl_cmds.cpp

@@ -28,7 +28,7 @@ static name g_colon(":");
 static name g_assign(":=");
 static name g_definition("definition");
 static name g_theorem("theorem");
-static name g_protected("[protected]");
+static name g_opaque("opaque");
 static name g_instance("[instance]");
 static name g_coercion("[coercion]");
 static name g_reducible("[reducible]");
@@ -162,12 +162,10 @@ environment axiom_cmd(parser & p)    {
 }
 
 struct decl_modifiers {
-    bool m_is_protected;
     bool m_is_instance;
     bool m_is_coercion;
     bool m_is_reducible;
     decl_modifiers() {
-        m_is_protected = false;
         m_is_instance  = false;
         m_is_coercion  = false;
         m_is_reducible = false;
@@ -175,10 +173,7 @@ struct decl_modifiers {
 
     void parse(parser & p) {
         while (true) {
-            if (p.curr_is_token(g_protected)) {
+            if (p.curr_is_token(g_instance)) {
-                m_is_protected = true;
-                p.next();
-            } else if (p.curr_is_token(g_instance)) {
                 m_is_instance = true;
                 p.next();
             } else if (p.curr_is_token(g_coercion)) {
@@ -204,14 +199,15 @@ static void erase_local_binder_info(buffer<expr> & ps) {
         p = update_local(p, binder_info());
 }
 
-environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, bool is_private) {
+environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, bool is_private, bool is_protected) {
+    lean_assert(!(is_theorem && !is_opaque));
+    lean_assert(!(is_private && !is_opaque));
+    lean_assert(!(is_private && is_protected));
     auto n_pos = p.pos();
     unsigned start_line = n_pos.first;
     name n     = p.check_id_next("invalid declaration, identifier expected");
     decl_modifiers modifiers;
     name real_n; // real name for this declaration
-    if (is_theorem)
-        is_opaque = true;
     buffer<name> ls_buffer;
     expr type, value;
     level_param_names ls;
@@ -353,21 +349,21 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo
         env = add_instance(env, real_n);
     if (modifiers.m_is_coercion)
         env = add_coercion(env, real_n, p.ios());
-    if (modifiers.m_is_protected)
+    if (is_protected)
         env = add_protected(env, real_n);
     if (modifiers.m_is_reducible)
         env = set_reducible(env, real_n, reducible_status::On);
     return env;
 }
 environment definition_cmd(parser & p) {
-    return definition_cmd_core(p, false, false, false);
+    return definition_cmd_core(p, false, false, false, false);
 }
 environment opaque_definition_cmd(parser & p) {
     p.check_token_next(g_definition, "invalid 'opaque' definition, 'definition' expected");
-    return definition_cmd_core(p, false, true, false);
+    return definition_cmd_core(p, false, true, false, false);
 }
 environment theorem_cmd(parser & p) {
-    return definition_cmd_core(p, true, true, false);
+    return definition_cmd_core(p, true, true, false, false);
 }
 environment private_definition_cmd(parser & p) {
     bool is_theorem = false;
@@ -379,7 +375,25 @@ environment private_definition_cmd(parser & p) {
     } else {
         throw parser_error("invalid 'private' definition/theorem, 'definition' or 'theorem' expected", p.pos());
     }
-    return definition_cmd_core(p, is_theorem, true, true);
+    return definition_cmd_core(p, is_theorem, true, true, false);
+}
+environment protected_definition_cmd(parser & p) {
+    bool is_theorem = false;
+    bool is_opaque  = false;
+    if (p.curr_is_token_or_id(g_opaque)) {
+        is_opaque = true;
+        p.next();
+        p.check_token_next(g_definition, "invalid 'protected' definition, 'definition' expected");
+    } else if (p.curr_is_token_or_id(g_definition)) {
+        p.next();
+    } else if (p.curr_is_token_or_id(g_theorem)) {
+        p.next();
+        is_theorem = true;
+        is_opaque  = true;
+    } else {
+        throw parser_error("invalid 'protected' definition/theorem, 'definition' or 'theorem' expected", p.pos());
+    }
+    return definition_cmd_core(p, is_theorem, is_opaque, false, true);
 }
 
 static name g_lparen("("), g_lcurly("{"), g_ldcurly("⦃"), g_lbracket("[");
@@ -426,6 +440,7 @@ void register_decl_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("definition",   "add new definition", definition_cmd));
     add_cmd(r, cmd_info("opaque",       "add new opaque definition", opaque_definition_cmd));
     add_cmd(r, cmd_info("private",      "add new private definition/theorem", private_definition_cmd));
+    add_cmd(r, cmd_info("protected",    "add new protected definition/theorem", protected_definition_cmd));
     add_cmd(r, cmd_info("theorem",      "add new theorem", theorem_cmd));
     add_cmd(r, cmd_info("variables",    "declare new parameters", variables_cmd));
 }

src/frontends/lean/token_table.cpp

@@ -77,8 +77,8 @@ token_table init_token_table() {
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"including", 0}, {"sorry", g_max_prec},
          {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
 
-    char const * commands[] = {"theorem", "axiom", "variable", "private", "opaque", "definition", "coercion",
+    char const * commands[] = {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "coercion",
-                               "variables", "[persistent]", "[protected]", "[visible]", "[instance]",
+                               "variables", "[persistent]", "[visible]", "[instance]",
                                "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "reducible",
                                "evaluate", "check", "print", "end", "namespace", "section", "import",
                                "inductive", "record", "renaming", "extends", "structure", "module", "universe",

tests/lean/interactive/coe.lean

@@ -1,7 +1,7 @@
 import data.int
 open int
 
-theorem has_decidable_eq [instance] [protected] : decidable_eq ℤ :=
+protected theorem has_decidable_eq [instance] : decidable_eq ℤ :=
 take (a b : ℤ), _
 
 variable n : nat

tests/lean/protected.lean

@@ -1,7 +1,7 @@
 import logic
 
 namespace foo
-  definition C [protected] := true
+  protected definition C := true
   definition D := true
 end foo
 

tests/lean/run/lift.lean

@@ -11,7 +11,7 @@ rec (λ a, a) a
 theorem down_up {A : Type} (a : A) : down (up a) = a :=
 rfl
 
-theorem induction_on [protected] {A : Type} {P : lift A → Prop} (a : lift A) (H : ∀ (a : A), P (up a)) : P a :=
+protected theorem induction_on {A : Type} {P : lift A → Prop} (a : lift A) (H : ∀ (a : A), P (up a)) : P a :=
 rec H a
 
 theorem up_down {A : Type} (a' : lift A) : up (down a') = a' :=

tests/lean/run/protected.lean

@@ -1,7 +1,7 @@
 import logic
 
 namespace foo
-  definition C [protected] := true
+  protected definition C := true
   definition D := true
 end foo