tactic.subtype_instance

source

def tactic.mk_mem_name (sub : name) :

name → name

makes the substructure axiom name from field name, by postfacing with _mem

Equations

tactic.mk_mem_name sub (name.mk_numeral ᾰ ᾰ_1) = name.mk_numeral ᾰ ᾰ_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

source

meta def tactic.derive_field_subtype :

tactic unit

source

meta def tactic.interactive.subtype_instance :

tactic unit

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
```