lean2/tests/lean/hott/610.hlean

import hit.quotient
attribute quotient.elim [recursor 6]

definition my_elim_on {A : Type} {R : A → A → Type} {P : Type} (x : quotient R)
                      (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') : P :=
begin
  induction x,
  exact Pc a,
  exact Pp H
end
renaming(hit): rename type_quotient to quotient, and quotient to set_quotient This renaming is because type_quotient is a nonstandard name. I've had a discussion with Egbert Rijke, Steve Awodey and Dan Licata, and the consensus for a better name was 'quotient'. I had to make changes in src/kernel/hits/hits.cpp, I renamed g_type_quotient* by g_hit_quotient* (to avoid name clash the standard library quotient, although I don't know whether that name clash would matter). 2015-06-04 15:57:00 -04:00			`import hit.quotient`
			`attribute quotient.elim [recursor 6]`
fix(library/tactic/induction_tactic): fixes #610 2015-05-20 20:28:02 -07:00
renaming(hit): rename type_quotient to quotient, and quotient to set_quotient This renaming is because type_quotient is a nonstandard name. I've had a discussion with Egbert Rijke, Steve Awodey and Dan Licata, and the consensus for a better name was 'quotient'. I had to make changes in src/kernel/hits/hits.cpp, I renamed g_type_quotient* by g_hit_quotient* (to avoid name clash the standard library quotient, although I don't know whether that name clash would matter). 2015-06-04 15:57:00 -04:00			`definition my_elim_on {A : Type} {R : A → A → Type} {P : Type} (x : quotient R)`
fix(library/tactic/induction_tactic): fixes #610 2015-05-20 20:28:02 -07:00			`(Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') : P :=`
			`begin`
			`induction x,`
			`exact Pc a,`
			`exact Pp H`
			`end`