Skip to content

chore: better error message in linarith#2605

Open
eric-wieser wants to merge 2 commits intomasterfrom
eric-wieser/linarith-exceptions
Open

chore: better error message in linarith#2605
eric-wieser wants to merge 2 commits intomasterfrom
eric-wieser/linarith-exceptions

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser commented Mar 3, 2023

On this mwe:

import Mathlib.Tactic.Linarith

example (s : Set ℕ) (h : s = s) : 0 ≤ 1 :=
by linarith

this now indicates where the internal error is coming from.

Is there a better way of chaining errors than this?

Open in Gitpod

@eric-wieser eric-wieser added the t-meta Tactics, attributes or user commands label Mar 3, 2023
@eric-wieser eric-wieser mentioned this pull request Mar 3, 2023
Closed
@Vierkantor
Copy link
Copy Markdown
Contributor

Vierkantor commented Mar 6, 2023

Is this equivalent to mathlib3's tactic.decorate_error? I found Std.Tactic.Lint.decorateError which seems to do the same, so I'd suggest using that (ideally after moving it to a more generic namespace.)

@kim-em kim-em added awaiting-review merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Apr 20, 2023
@Parcly-Taxel Parcly-Taxel removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 20, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 24, 2023

@eric-wieser do you want to do anything about Anne's comment, or proceed as is?

@kim-em kim-em added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Apr 24, 2023
@bors bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:23
@kim-em kim-em changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 12:18
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 22, 2023
@harahu
Copy link
Copy Markdown
Contributor

harahu commented Jan 30, 2025

Is this PR abandoned? I'm noticing it hasn't been touched for quite some time. One might as well close it if that is the case.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@mo271 mo271 mo271 approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

awaiting-author A reviewer has asked the author a question or requested changes. merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@eric-wieser @Vierkantor @kim-em @harahu @mo271 @Parcly-Taxel