lean2/tests/lean/struct_class.lean.expected.out

decidable : Prop → Type₁
has_add : Type → Type
has_div : Type → Type
has_dvd : Type → Type
has_inv : Type → Type
has_le : Type → Type
has_lt : Type → Type
has_mod : Type → Type
has_mul : Type → Type
has_neg : Type → Type
has_one : Type → Type
has_sub : Type → Type
has_zero : Type → Type
inhabited : Type → Type
measurable : Type → Type
nonempty : Type → Prop
point : Type → Type → Type
setoid : Type → Type
subsingleton : Type → Prop
well_founded : Π {A}, (A → A → Prop) → Prop
decidable : Prop → Type₁
has_add : Type → Type
has_div : Type → Type
has_dvd : Type → Type
has_inv : Type → Type
has_le : Type → Type
has_lt : Type → Type
has_mod : Type → Type
has_mul : Type → Type
has_neg : Type → Type
has_one : Type → Type
has_sub : Type → Type
has_zero : Type → Type
inhabited : Type → Type
measurable : Type → Type
nonempty : Type → Prop
point : Type → Type → Type
setoid : Type → Type
subsingleton : Type → Prop
well_founded : Π {A}, (A → A → Prop) → Prop
fix(tests/lean): adjust tests to modifications to standard library 2014-12-01 05:16:01 +00:00			`decidable : Prop → Type₁`
fix(tests/lean): adjust remaining tests to changes in the standard library 2015-10-14 01:35:16 +00:00			`has_add : Type → Type`
refactor(library/*): use type classes for div and mod 2015-10-29 19:36:26 +00:00			`has_div : Type → Type`
fix(tests/lean): adjust remaining tests to changes in the standard library 2015-10-14 01:35:16 +00:00			`has_dvd : Type → Type`
			`has_inv : Type → Type`
			`has_le : Type → Type`
			`has_lt : Type → Type`
refactor(library/*): use type classes for div and mod 2015-10-29 19:36:26 +00:00			`has_mod : Type → Type`
fix(tests/lean): adjust remaining tests to changes in the standard library 2015-10-14 01:35:16 +00:00			`has_mul : Type → Type`
			`has_neg : Type → Type`
			`has_one : Type → Type`
			`has_sub : Type → Type`
			`has_zero : Type → Type`
fix(tests/lean): adjust tests to modifications to standard library 2014-12-01 05:16:01 +00:00			`inhabited : Type → Type`
fix(tests/lean/struct_class): adjust test result to reflect recent changes 2014-12-04 04:32:33 +00:00			`measurable : Type → Type`
fix(tests/lean): adjust tests to modifications to standard library 2014-12-01 05:16:01 +00:00			`nonempty : Type → Prop`
feat(frontends/lean/structure_cmd): mark structure as 'class' when [class] modifier is used 2014-11-04 01:46:03 +00:00			`point : Type → Type → Type`
fix(tests/lean/struct_class): add setoid to expected output 2015-04-01 04:53:49 +00:00			`setoid : Type → Type`
fix(tests/lean): adjust tests to reflect changes in the standard library 2015-04-01 22:09:00 +00:00			`subsingleton : Type → Prop`
chore(tests): mass-update for pp.binder_types false 2016-06-01 02:14:42 +00:00			`well_founded : Π {A}, (A → A → Prop) → Prop`
fix(tests/lean): adjust tests to modifications to standard library 2014-12-01 05:16:01 +00:00			`decidable : Prop → Type₁`
fix(tests/lean): adjust remaining tests to changes in the standard library 2015-10-14 01:35:16 +00:00			`has_add : Type → Type`
refactor(library/*): use type classes for div and mod 2015-10-29 19:36:26 +00:00			`has_div : Type → Type`
fix(tests/lean): adjust remaining tests to changes in the standard library 2015-10-14 01:35:16 +00:00			`has_dvd : Type → Type`
			`has_inv : Type → Type`
			`has_le : Type → Type`
			`has_lt : Type → Type`
refactor(library/*): use type classes for div and mod 2015-10-29 19:36:26 +00:00			`has_mod : Type → Type`
fix(tests/lean): adjust remaining tests to changes in the standard library 2015-10-14 01:35:16 +00:00			`has_mul : Type → Type`
			`has_neg : Type → Type`
			`has_one : Type → Type`
			`has_sub : Type → Type`
			`has_zero : Type → Type`
fix(tests/lean): adjust tests to modifications to standard library 2014-12-01 05:16:01 +00:00			`inhabited : Type → Type`
fix(tests/lean/struct_class): adjust test result to reflect recent changes 2014-12-04 04:32:33 +00:00			`measurable : Type → Type`
fix(tests/lean): adjust tests to modifications to standard library 2014-12-01 05:16:01 +00:00			`nonempty : Type → Prop`
feat(frontends/lean/structure_cmd): mark structure as 'class' when [class] modifier is used 2014-11-04 01:46:03 +00:00			`point : Type → Type → Type`
fix(tests/lean/struct_class): add setoid to expected output 2015-04-01 04:53:49 +00:00			`setoid : Type → Type`
fix(tests/lean): adjust tests to reflect changes in the standard library 2015-04-01 22:09:00 +00:00			`subsingleton : Type → Prop`
chore(tests): mass-update for pp.binder_types false 2016-06-01 02:14:42 +00:00			`well_founded : Π {A}, (A → A → Prop) → Prop`