mathlib3
[Merged by Bors] - fix(tactic/linarith): instantiate metavariables in linarith
#19233

Closed

[Merged by Bors] - fix(tactic/linarith): instantiate metavariables in linarith #19233

eric-wieser wants to merge 1 commit into master from eric-wieser/linarith-mvars-fix

fix(tactic/linarith): instantiate metavariables in linarith

e9ce2e99

eric-wieser added awaiting-review

eric-wieser added t-meta

eric-wieser added awaiting-CI

eric-wieser requested a review 2 years ago

kmill approved these changes on 2023-07-11

github-actions removed awaiting-CI

eric-wieser added not-too-late

github-actions added ready-to-merge

github-actions removed awaiting-review

bors changed the title ~~fix(tactic/linarith): instantiate metavariables in linarith~~ [Merged by Bors] - fix(tactic/linarith): instantiate metavariables in linarith 2 years ago

bors closed this 2 years ago

bors deleted the eric-wieser/linarith-mvars-fix branch 2 years ago

Reviewers

kmill

Assignees

No one assigned

Labels

ready-to-merge t-meta not-too-late

Milestone

No milestone

mathlib3 [Merged by Bors] - fix(tactic/linarith): instantiate metavariables in linarith #19233 Closed

[Merged by Bors] - fix(tactic/linarith): instantiate metavariables in linarith #19233

mathlib3
[Merged by Bors] - fix(tactic/linarith): instantiate metavariables in linarith
#19233

Closed