Skip to content

Commit

Permalink
doc(data/set_like/basic): tidy up docstring (#12337)
Browse files Browse the repository at this point in the history
Hopefully this makes the docstring slightly clearer.
  • Loading branch information
kbuzzard committed Feb 27, 2022
1 parent dfacfd3 commit 2f86b49
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions src/data/set_like/basic.lean
Expand Up @@ -27,16 +27,16 @@ boilerplate for every `set_like`: a `coe_sort`, a `coe` to set, a
A typical subobject should be declared as:
```
structure my_subobject (X : Type*) :=
structure my_subobject (X : Type*) [object_typeclass X] :=
(carrier : set X)
(op_mem : ∀ {x : X}, x ∈ carrier → sorry ∈ carrier)
(op_mem' : ∀ {x : X}, x ∈ carrier → sorry ∈ carrier)
namespace my_subobject
variables (X : Type*)
variables {X : Type*} [object_typeclass X] {x : X}
instance : set_like (my_subobject X) X :=
sub_mul_action.carrier, λ p q h, by cases p; cases q; congr'⟩
my_subobject.carrier, λ p q h, by cases p; cases q; congr'⟩
@[simp] lemma mem_carrier {p : my_subobject X} : x ∈ p.carrier ↔ x ∈ (p : set X) := iff.rfl
Expand Down

0 comments on commit 2f86b49

Please sign in to comment.