mathlib3
feat(meta/pformat): format! macro using `pp` instead of `to_fmt`
#1194

Merged

feat(meta/pformat): format! macro using `pp` instead of `to_fmt` #1194

mergify merged 3 commits into master from pp_format

feat(meta/pformat): format! macro which uses `pp` instead of `to_fmt`

06b010f6

cipher1024 requested a review 6 years ago

cipher1024 changed the title ~~feat(meta/pformat): format! macro which uses `pp` instead of `to_fmt`~~ feat(meta/pformat): format! macro using `pp` instead of `to_fmt` 6 years ago

Update core.lean

99afafcf

robertylewis approved these changes on 2019-07-09

robertylewis added ready-to-merge

Merge branch 'master' into pp_format

10d83ad4

mergify merged 0cd0d4ed into master 6 years ago

mergify deleted the pp_format branch 6 years ago

Reviewers

robertylewis

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone

mathlib3 feat(meta/pformat): format! macro using `pp` instead of `to_fmt` #1194 Merged

feat(meta/pformat): format! macro using `pp` instead of `to_fmt` #1194

mathlib3
feat(meta/pformat): format! macro using `pp` instead of `to_fmt`
#1194

Merged