chore(library/init/quot): annotate quot eliminators

library/init/quot.lean

@@ -26,6 +26,8 @@ namespace quot
   constant lift      : Π {A B : Type} [s : setoid A] (f : A → B), (∀ a b, a ≈ b → f a = f b) → quot s → B
   constant ind       : ∀ {A : Type}   [s : setoid A] {B : quot s → Prop}, (∀ a, B ⟦a⟧) → ∀ q, B q
 
+  attribute [elab_as_eliminator] lift ind
+
   init_quotient
 
   protected theorem lift_beta {A B : Type} [setoid A] (f : A → B) (c : ∀ a b, a ≈ b → f a = f b) (a : A) : lift f c ⟦a⟧ = f a :=
@@ -34,10 +36,11 @@ namespace quot
   protected theorem ind_beta {A : Type} [s : setoid A] {B : quot s → Prop} (p : ∀ a, B ⟦a⟧) (a : A) : ind p ⟦a⟧ = p a :=
   rfl
 
-  attribute [reducible]
+  attribute [reducible, elab_as_eliminator]
   protected definition lift_on {A B : Type} [s : setoid A] (q : quot s) (f : A → B) (c : ∀ a b, a ≈ b → f a = f b) : B :=
   lift f c q
 
+  attribute [elab_as_eliminator]
   protected theorem induction_on {A : Type} [s : setoid A] {B : quot s → Prop} (q : quot s) (H : ∀ a, B ⟦a⟧) : B q :=
   ind H q
 
@@ -64,23 +67,23 @@ namespace quot
     (q : quot s) : (lift (quot.indep f) (quot.indep_coherent f H) q).1 = q  :=
   quot.ind (λ (a : A), eq.refl (quot.indep f a).1) q
 
-  attribute [reducible]
+  attribute [reducible, elab_as_eliminator]
   protected definition rec
      (f : Π a, B ⟦a⟧) (H : ∀ (a b : A) (p : a ≈ b), eq.rec (f a) (sound p) = f b)
      (q : quot s) : B q :=
   eq.rec_on (quot.lift_indep_pr1 f H q) ((lift (quot.indep f) (quot.indep_coherent f H) q).2)
 
-  attribute [reducible]
+  attribute [reducible, elab_as_eliminator]
   protected definition rec_on
      (q : quot s) (f : Π a, B ⟦a⟧) (H : ∀ (a b : A) (p : a ≈ b), eq.rec (f a) (sound p) = f b) : B q :=
   quot.rec f H q
 
-  attribute [reducible]
+  attribute [reducible, elab_as_eliminator]
   protected definition rec_on_subsingleton
      [H : ∀ a, subsingleton (B ⟦a⟧)] (q : quot s) (f : Π a, B ⟦a⟧) : B q :=
   quot.rec f (λ a b h, subsingleton.elim _ (f b)) q
 
-  attribute [reducible]
+  attribute [reducible, elab_as_eliminator]
   protected definition hrec_on
      (q : quot s) (f : Π a, B ⟦a⟧) (c : ∀ (a b : A) (p : a ≈ b), f a == f b) : B q :=
   quot.rec_on q f
@@ -94,7 +97,7 @@ namespace quot
   variables [s₁ : setoid A] [s₂ : setoid B]
   include s₁ s₂
 
-  attribute [reducible]
+  attribute [reducible, elab_as_eliminator]
   protected definition lift₂
      (f : A → B → C)(c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂)
      (q₁ : quot s₁) (q₂ : quot s₂) : C :=
@@ -110,18 +113,21 @@ namespace quot
          q₂)
     q₁
 
-  attribute [reducible]
+  attribute [reducible, elab_as_eliminator]
   protected definition lift_on₂
     (q₁ : quot s₁) (q₂ : quot s₂) (f : A → B → C) (c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) : C :=
   quot.lift₂ f c q₁ q₂
 
+  attribute [elab_as_eliminator]
   protected theorem ind₂ {C : quot s₁ → quot s₂ → Prop} (H : ∀ a b, C ⟦a⟧ ⟦b⟧) (q₁ : quot s₁) (q₂ : quot s₂) : C q₁ q₂ :=
   quot.ind (λ a₁, quot.ind (λ a₂, H a₁ a₂) q₂) q₁
 
+  attribute [elab_as_eliminator]
   protected theorem induction_on₂
      {C : quot s₁ → quot s₂ → Prop} (q₁ : quot s₁) (q₂ : quot s₂) (H : ∀ a b, C ⟦a⟧ ⟦b⟧) : C q₁ q₂ :=
   quot.ind (λ a₁, quot.ind (λ a₂, H a₁ a₂) q₂) q₁
 
+  attribute [elab_as_eliminator]
   protected theorem induction_on₃
      [s₃ : setoid C]
      {D : quot s₁ → quot s₂ → quot s₃ → Prop} (q₁ : quot s₁) (q₂ : quot s₂) (q₃ : quot s₃) (H : ∀ a b c, D ⟦a⟧ ⟦b⟧ ⟦c⟧)
@@ -160,7 +166,7 @@ namespace quot
   include s₁ s₂
   variable {C : quot s₁ → quot s₂ → Type}
 
-  attribute [reducible]
+  attribute [reducible, elab_as_eliminator]
   protected definition rec_on_subsingleton₂
      {C : quot s₁ → quot s₂ → Type} [H : ∀ a b, subsingleton (C ⟦a⟧ ⟦b⟧)]
      (q₁ : quot s₁) (q₂ : quot s₂) (f : Π a b, C ⟦a⟧ ⟦b⟧) : C q₁ q₂:=
@@ -168,7 +174,7 @@ namespace quot
     (λ a, quot.ind _ _)
     q₁ (λ a, quot.rec_on_subsingleton q₂ (λ b, f a b))
 
-  attribute [reducible]
+  attribute [reducible, elab_as_eliminator]
   protected definition hrec_on₂
      {C : quot s₁ → quot s₂ → Type} (q₁ : quot s₁) (q₂ : quot s₂)
      (f : Π a b, C ⟦a⟧ ⟦b⟧) (c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ == f b₁ b₂) : C q₁ q₂:=

tests/lean/quot_ind_bug.lean

@@ -1,6 +1,6 @@
 open quot
 
 variables {A : Type} [s : setoid A] {B : quot s → Prop} (c : ∀ (a : A), B (quot.mk a)) (a : A)
-check quot.ind c ⟦a⟧
+check (quot.ind c ⟦a⟧ : B ⟦a⟧)
 check c a
-eval quot.ind c ⟦a⟧
+eval (quot.ind c ⟦a⟧ : B ⟦a⟧)