[Merged by Bors] - feat(library/init/logic): mark dif_ctx_congr as @[congr]

[semorrison]

mathlib still compiles, and we can simplify inside the condition of a dite:

inductive A (α : Type)
| mk : α → A

@[instance] axiom classical {α : Type} : decidable_eq α

example {α : Type} (a b : α) :
  (if h : A.mk a = A.mk b then true else false) ↔ (if h : a = b then true else false) :=
begin
  simp, -- fails
end

attribute [congr] dif_ctx_congr

example {α : Type} (a b : α) :
  (if h : A.mk a = A.mk b then true else false) ↔ (if h : a = b then true else false) :=
begin
  simp, -- succeeds
end

The example where I wanted this to work actually using the hypothesis h in the branches, and it now works fine.

[cipher1024]

Have you tried building mathlib with it?

[bryangingechen]

Have you tried building mathlib with it?

The first sentence of the PR is "mathlib still compiles", right?

[cipher1024]

Right, I should read more carefully. This looks good to me. I haven't reviewed a PR for a while. What is the new way of putting one on the build queue?

[bryangingechen]

You can type bors r+ or equivalently bors merge on its own line in a comment or PR review comment. The PR then gets added to the queue which you can view here (more docs on that page too).

[cipher1024]

Nice! Thanks! So by you explaining it to me, you actually accepted the PR, right?

[bryangingechen]

No, I didn't put the command on its own line. Didn't want to keep all the fun for myself. 😉

[cipher1024]

Here we go then!

[cipher1024]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build windows Release
• Build linux Release
• Build macos Debug
• Build linux Debug
• Build emscripten
• Build macos Release