diff --git a/doc/changes.md b/doc/changes.md index 265b703b9a..8089d849ce 100644 --- a/doc/changes.md +++ b/doc/changes.md @@ -38,6 +38,8 @@ master branch (aka work in progress branch) - Add support for structure instance notation `{...}` in patterns. Use `..` to ignore unmatched fields. +- Type class has_equiv for `≈` notation. + *Changes* - `string` is now a list of unicode scalar values. Moreover, in the VM, diff --git a/library/init/core.lean b/library/init/core.lean index 99e086a255..0b4bb36984 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -315,6 +315,7 @@ class has_andthen (α : Type u) (β : Type v) (σ : inout Type w) := (andthen : class has_union (α : Type u) := (union : α → α → α) class has_inter (α : Type u) := (inter : α → α → α) class has_sdiff (α : Type u) := (sdiff : α → α → α) +class has_equiv (α : Sort u) := (equiv : α → α → Prop) class has_subset (α : Type u) := (subset : α → α → Prop) class has_ssubset (α : Type u) := (ssubset : α → α → Prop) /- Type classes has_emptyc and has_insert are @@ -351,6 +352,7 @@ infix ∩ := has_inter.inter infix ⊆ := has_subset.subset infix ⊂ := has_ssubset.ssubset infix \ := has_sdiff.sdiff +infix ≈ := has_equiv.equiv export has_append (append) diff --git a/library/init/data/setoid.lean b/library/init/data/setoid.lean index e6459853ee..f5bcbc1487 100644 --- a/library/init/data/setoid.lean +++ b/library/init/data/setoid.lean @@ -10,14 +10,15 @@ universes u class setoid (α : Sort u) := (r : α → α → Prop) (iseqv : equivalence r) -namespace setoid -infix ` ≈ ` := setoid.r +instance setoid_has_equiv {α : Sort u} [setoid α] : has_equiv α := +⟨setoid.r⟩ +namespace setoid variable {α : Sort u} variable [s : setoid α] include s -@[refl] lemma refl (a : α) : a ≈ a := +@[refl] lemma refl [setoid α] (a : α) : a ≈ a := match setoid.iseqv α with | ⟨h_refl, h_symm, h_trans⟩ := h_refl a end diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out index 3842c9920d..4f6898d6cc 100644 --- a/tests/lean/struct_class.lean.expected.out +++ b/tests/lean/struct_class.lean.expected.out @@ -5,6 +5,7 @@ has_append : Type u → Type u has_div : Type u → Type u has_dvd : Type u → Type u has_emptyc : Type u → Type u +has_equiv : Sort u → Sort (max 1 u) has_insert : (inout Type u) → Type v → Type (max u v) has_inter : Type u → Type u has_inv : Type u → Type u @@ -31,6 +32,7 @@ has_append : Type u → Type u has_div : Type u → Type u has_dvd : Type u → Type u has_emptyc : Type u → Type u +has_equiv : Sort u → Sort (max 1 u) has_insert : (inout Type u) → Type v → Type (max u v) has_inter : Type u → Type u has_inv : Type u → Type u