From 0d99c92886d3cdc154f01c228adbd649f384ee2b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Oct 2020 05:34:26 -0700 Subject: [PATCH] chore: use `motive` to name the motive of `Eq.ndrec` and friends --- src/Init/Core.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 6f1c3d35ce..2c7dac6471 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -166,12 +166,12 @@ inductive Eq {α : Sort u} (a : α) : α → Prop | refl {} : Eq a @[elabAsEliminator, inline, reducible] -def Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {C : α → Sort u1} (m : C a) {b : α} (h : Eq a b) : C b := -@Eq.rec α a (fun α _ => C α) m b h +def Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b := +@Eq.rec α a (fun α _ => motive α) m b h @[elabAsEliminator, inline, reducible] -def Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {C : α → Sort u1} {b : α} (h : Eq a b) (m : C a) : C b := -@Eq.rec α a (fun α _ => C α) m b h +def Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : Eq a b) (m : motive a) : motive b := +@Eq.rec α a (fun α _ => motive α) m b h /- Initialize the Quotient Module, which effectively adds the following definitions: @@ -744,12 +744,12 @@ section variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ} @[elabAsEliminator] -theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {C : ∀ {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β} (h : a ≅ b) : C b := -@HEq.rec α a (fun β b _ => C b) m β b h +theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : ∀ {β : Sort u2}, β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : a ≅ b) : motive b := +@HEq.rec α a (fun β b _ => motive b) m β b h @[elabAsEliminator] -theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {C : ∀ {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : C a) : C b := -@HEq.rec α a (fun β b _ => C b) m β b h +theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : ∀ {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : motive a) : motive b := +@HEq.rec α a (fun β b _ => motive b) m β b h theorem HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b := Eq.recOn (eqOfHEq h₁) h₂