diff --git a/library/algebra/group.lean b/library/algebra/group.lean index 06d227366..f2be1ea9f 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -42,8 +42,8 @@ infixl `*` := has_mul.mul infixl `+` := has_add.add postfix `⁻¹` := has_inv.inv prefix `-` := has_neg.neg -notation 1 := has_one.one -notation 0 := has_zero.zero +notation 1 := !has_one.one +notation 0 := !has_zero.zero /- semigroup -/ diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index 39e8a5ef8..11af1037f 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -161,7 +161,7 @@ structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_ definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] (A : Type) [s : ordered_comm_group A] : ordered_cancel_comm_monoid A := -ordered_cancel_comm_monoid.mk has_add.add add_assoc has_zero.zero add_left_id add_right_id add_comm +ordered_cancel_comm_monoid.mk has_add.add add_assoc !has_zero.zero add_left_id add_right_id add_comm (@add_left_cancel _ _) (@add_right_cancel _ _) has_le.le le_refl (@le_trans _ _) (@le_antisym _ _) has_lt.lt (@lt_iff_le_ne _ _) ordered_comm_group.add_le_left proof diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 663739c5c..7f1410c50 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -38,8 +38,7 @@ theorem mul_zero_right [s : mul_zero A] (a : A) : a * 0 = 0 := !mul_zero.mul_zer structure zero_ne_one_class [class] (A : Type) extends has_zero A, has_one A := (zero_ne_one : zero ≠ one) -theorem zero_ne_one [s: zero_ne_one_class A] : 0 ≠ 1 := zero_ne_one_class.zero_ne_one - +theorem zero_ne_one [s: zero_ne_one_class A] : 0 ≠ 1 := !zero_ne_one_class.zero_ne_one /- semiring -/ structure semiring [class] (A : Type) extends add_comm_monoid A, monoid A, distrib A, mul_zero A, @@ -150,9 +149,9 @@ end comm_semiring_dvd structure ring [class] (A : Type) extends add_comm_group A, monoid A, distrib A, zero_ne_one_class A definition ring.to_semiring [instance] [s : ring A] : semiring A := -semiring.mk ring.add ring.add_assoc ring.zero ring.add_left_id +semiring.mk ring.add ring.add_assoc !ring.zero ring.add_left_id add_right_id -- note: we've shown that add_right_id follows from add_left_id in add_comm_group - ring.add_comm ring.mul ring.mul_assoc ring.one ring.mul_left_id ring.mul_right_id + ring.add_comm ring.mul ring.mul_assoc !ring.one ring.mul_left_id ring.mul_right_id ring.distrib_left ring.distrib_right (take a, have H : 0 * a + 0 = 0 * a + 0 * a, from @@ -168,7 +167,7 @@ semiring.mk ring.add ring.add_assoc ring.zero ring.add_left_id ... = a * (0 + 0) : add_right_id ... = a * 0 + a * 0 : ring.distrib_left, show a * 0 = 0, from (add_left_cancel H)⁻¹) - ring.zero_ne_one + !ring.zero_ne_one section @@ -224,8 +223,8 @@ end structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A definition comm_ring.to_comm_semiring [instance] [s : comm_ring A] : comm_semiring A := -comm_semiring.mk has_add.add add_assoc has_zero.zero add_left_id add_right_id add_comm - has_mul.mul mul_assoc has_one.one mul_left_id mul_right_id distrib_left distrib_right +comm_semiring.mk has_add.add add_assoc !has_zero.zero add_left_id add_right_id add_comm + has_mul.mul mul_assoc !has_one.one mul_left_id mul_right_id distrib_left distrib_right mul_zero_left mul_zero_right zero_ne_one mul_comm section @@ -244,8 +243,8 @@ end structure comm_ring_dvd [class] (A : Type) extends comm_ring A, has_dvd A definition comm_ring_dvd.to_comm_semiring_dvd [instance] [s : comm_ring_dvd A] : comm_semiring_dvd A := -comm_semiring_dvd.mk has_add.add add_assoc has_zero.zero add_left_id add_right_id add_comm - has_mul.mul mul_assoc has_one.one mul_left_id mul_right_id distrib_left distrib_right +comm_semiring_dvd.mk has_add.add add_assoc !has_zero.zero add_left_id add_right_id add_comm + has_mul.mul mul_assoc !has_one.one mul_left_id mul_right_id distrib_left distrib_right mul_zero_left mul_zero_right zero_ne_one mul_comm dvd (@dvd_intro A s) (@dvd_imp_exists A s) section diff --git a/library/hott/trunc.lean b/library/hott/trunc.lean index f9df0ac8a..4cf136528 100644 --- a/library/hott/trunc.lean +++ b/library/hott/trunc.lean @@ -81,11 +81,11 @@ namespace truncation -- maybe rename to is_trunc_succ.mk definition is_trunc_succ (A : Type) {n : trunc_index} [H : ∀x y : A, is_trunc n (x ≈ y)] : is_trunc n.+1 A := - is_trunc.mk (λ x y, is_trunc.to_internal) + is_trunc.mk (λ x y, !is_trunc.to_internal) -- maybe rename to is_trunc_succ.elim definition succ_is_trunc {n : trunc_index} [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x ≈ y) := - is_trunc.mk (is_trunc.to_internal x y) + is_trunc.mk (!is_trunc.to_internal x y) /- contractibility -/ @@ -93,10 +93,10 @@ namespace truncation is_trunc.mk (contr_internal.mk center contr) definition center (A : Type) [H : is_contr A] : A := - @contr_internal.center A is_trunc.to_internal + @contr_internal.center A !is_trunc.to_internal definition contr [H : is_contr A] (a : A) : !center ≈ a := - @contr_internal.contr A is_trunc.to_internal a + @contr_internal.contr A !is_trunc.to_internal a definition path_contr [H : is_contr A] (x y : A) : x ≈ y := contr x⁻¹ ⬝ (contr y) diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp index 424ae854b..26790b8ff 100644 --- a/src/library/definitional/projection.cpp +++ b/src/library/definitional/projection.cpp @@ -107,7 +107,7 @@ environment mk_projections(environment const & env, name const & n, buffer rec_args.push_back(major_premise); expr rec_app = mk_app(rec, rec_args); expr proj_type = Pi(proj_args, result_type); - bool strict = false; + bool strict = true; proj_type = infer_implicit(proj_type, nparams, strict); expr proj_val = Fun(proj_args, rec_app); bool opaque = false; diff --git a/tests/lean/run/group4.lean b/tests/lean/run/group4.lean index f9c17c88d..9f72786ed 100644 --- a/tests/lean/run/group4.lean +++ b/tests/lean/run/group4.lean @@ -26,7 +26,7 @@ mk :: (inv : A → A) infixl `*` := has_mul.mul postfix `⁻¹` := has_inv.inv -notation 1 := has_one.one +notation 1 := !has_one.one structure semigroup [class] (A : Type) extends has_mul A := mk :: (assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c)) diff --git a/tests/lean/run/group5.lean b/tests/lean/run/group5.lean index a85db5a0e..283a79191 100644 --- a/tests/lean/run/group5.lean +++ b/tests/lean/run/group5.lean @@ -26,7 +26,7 @@ structure has_inv [class] (A : Type) := infixl `*` := has_mul.mul postfix `⁻¹` := has_inv.inv -notation 1 := has_one.one +notation 1 := !has_one.one structure semigroup [class] (A : Type) extends has_mul A := (assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c))