Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-10 15:51 2cd59b41

View on Github →

feat(coinduction): add identifier list to coinduction tactic (#1653)

feat(coinduction): add identifier list to coinduction tactic
Update coinductive_predicates.lean
two doc strings [skip ci]
Update coinductive_predicates.lean
fix merge
move definitions around
move more stuff
fix build
move and document functions

Estimated changes

Modified src/meta/coinductive_predicates.lean

deleted def name.last_string

Modified src/meta/expr.lean

added def name.last_string

Modified src/tactic/core.lean

Modified src/tactic/mk_iff_of_inductive_prop.lean

Modified test/examples.lean