makes the substructure axiom name from field name, by postfacing with _mem
Equations
- tactic.mk_mem_name sub (name.mk_numeral a a_1) = name.mk_numeral a a_1
- tactic.mk_mem_name sub (name.mk_string n _x) = name.mk_string (n ++ "_mem") sub
- tactic.mk_mem_name sub name.anonymous = name.anonymous
builds instances for algebraic substructures
Example:
variables {α : Type*} [monoid α] {s : set α}
class is_submonoid (s : set α) : Prop :=
(one_mem : (1:α) ∈ s)
(mul_mem {a b} : a ∈ s → b ∈ s → a * b ∈ s)
instance subtype.monoid {s : set α} [is_submonoid s] : monoid s :=
by subtype_instance