PR #2063 feat(tactic/tidy): include norm_cast in tidy

feat(tactic/tidy): include norm_cast in tidy #2063

mergify merged 4 commits into master from tidy_norm_cast

feat(tactic/tidy): include norm_cast in tidy

ba7851be

robertylewis approved these changes on 2020-02-27

Update src/tactic/core.lean

a11b5bf1

robertylewis added ready-to-merge

Merge branch 'master' into tidy_norm_cast

ef7cfd38

Merge branch 'master' into tidy_norm_cast

b27369c5

mergify merged 7907f8f3 into master 5 years ago

mergify deleted the tidy_norm_cast branch 5 years ago

Reviewers

robertylewis

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone