Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-02 17:21 3de3cfb3

View on Github →

feat(tactic/subtype_instance): generating subtype instances

Estimated changes

Modified data/list/basic.lean

added def list.map_head

added def list.map_last

Modified data/string.lean

added def string.map_tokens

Created field_theory/subfield.lean

Modified group_theory/subgroup.lean

Modified group_theory/submonoid.lean

Created ring_theory/subring.lean

Created tactic/algebra.lean

Modified tactic/basic.lean

Created tactic/subtype_instance.lean

added def tactic.mk_mem_name