Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Diamonds at reducible_and_instances transparency #10906

Open
mattrobball opened this issue Feb 24, 2024 · 0 comments
Open

Diamonds at reducible_and_instances transparency #10906

mattrobball opened this issue Feb 24, 2024 · 0 comments

Comments

@mattrobball
Copy link
Collaborator

There are diamonds at the transparency settings used by typeclass synthesis and simp which are fine at default transparency.

Some have checks in the file which use := rfl and not := by with_reducible_and_instances rfl.
@mattrobball mattrobball mentioned this issue Feb 24, 2024
Closed
mathlib-bors bot pushed a commit that referenced this issue Feb 24, 2024
@mattrobball @kbuzzard
chore(diamonds): appropriate transparency levels for diamond checks (#…
29c854d 
…10910)

Currently, we have multiple "no-diamond" tests of the form
```lean
example : x = y := rfl
```
where `X` and `Y` are instances of some `class`. The problem is that since `simp` and type class synthesis operate at `reducible_and_instances` transparency this check means little.

We went through all the mentions of diamonds and either added `with_reducible_and_instancse` or added a reference to the issue #10906.



Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
riccardobrasca pushed a commit that referenced this issue Mar 1, 2024
@mattrobball @kbuzzard @riccardobrasca
chore(diamonds): appropriate transparency levels for diamond checks (#…
056a9d1 
…10910)

Currently, we have multiple "no-diamond" tests of the form
```lean
example : x = y := rfl
```
where `X` and `Y` are instances of some `class`. The problem is that since `simp` and type class synthesis operate at `reducible_and_instances` transparency this check means little.

We went through all the mentions of diamonds and either added `with_reducible_and_instancse` or added a reference to the issue #10906.



Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
dagurtomas pushed a commit that referenced this issue Mar 22, 2024
@mattrobball @kbuzzard @dagurtomas
chore(diamonds): appropriate transparency levels for diamond checks (#…
1cef6bd 
…10910)

Currently, we have multiple "no-diamond" tests of the form
```lean
example : x = y := rfl
```
where `X` and `Y` are instances of some `class`. The problem is that since `simp` and type class synthesis operate at `reducible_and_instances` transparency this check means little.

We went through all the mentions of diamonds and either added `with_reducible_and_instancse` or added a reference to the issue #10906.



Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Louddy pushed a commit that referenced this issue Apr 15, 2024
@mattrobball @kbuzzard @Louddy
chore(diamonds): appropriate transparency levels for diamond checks (#…
5c66432 
…10910)

Currently, we have multiple "no-diamond" tests of the form
```lean
example : x = y := rfl
```
where `X` and `Y` are instances of some `class`. The problem is that since `simp` and type class synthesis operate at `reducible_and_instances` transparency this check means little.

We went through all the mentions of diamonds and either added `with_reducible_and_instancse` or added a reference to the issue #10906.



Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@mattrobball