mathlib3
feat(tactic/basic): utility functions for names
#791
Merged

feat(tactic/basic): utility functions for names #791

cipher1024 merged 1 commit into master from tactic-basic-name
kim-em
kim-em feat(tactic/basic): utility functions for names
bfa76b76
kim-em kim-em requested a review from digama0 digama0 6 years ago
cipher1024 cipher1024 assigned digama0 digama0 6 years ago
digama0
digama0 approved these changes on 2019-03-06
cipher1024 cipher1024 merged 181647bb into master 6 years ago
kim-em kim-em deleted the tactic-basic-name branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
Labels
Milestone