cannot remove attribute [class]

Stream: general

[Kevin Buzzard]

local attribute [-class] decidable -- cannot remove attribute [class]

I assume there's a good reason for this? I wanted to do it because someone on the Discord was asking why they got a weird error when they did cases h when h : decidable p and I wanted to demonstrate a very bad way of working around the issue (after explaining unfreezingI first!)

[Gabriel Ebner]

It's because it takes extra work to implement it, and I think this is the first time anybody every asked for it.

[Eric Rodriguez]

I thought the same when I ran into the error, but I assumed whoever wrote Lean knew better than me

[Kevin Buzzard]

I certainly don't need it :-) As I say, it just seemed to be the quickest way of proving the assertion "your code (casing on a frozen local instance) doesn't work because decidable is a class".