max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: use motive to name the motive of Eq.ndrec and friends

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-23 05:34:26 -07:00
parent ec17fcbc1a
commit 0d99c92886
1 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/Init/Core.lean
View file

@ -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₂