tidy subtype

Stream: general

[Yury G. Kudryashov]

Does tidy have some kind of special support for subtypes?

[Johan Commelin]

Not that I know of. Probably ext takes care of things?

[Yury G. Kudryashov]

I changed docs#topological_space.opens to a structure (like docs#topological_space.closeds) and some tidys in category_theory fail.

[Johan Commelin]

Weird :shrug:

[Yury G. Kudryashov]

Found it! tactic#auto_cases has a list of types it runs cases on.

[Yury G. Kudryashov]

I don't know how to fix it.

[Yury G. Kudryashov]

@Mario Carneiro :up:

[Yury G. Kudryashov]

Should I write something like tactic.op_induction'?

[Mario Carneiro]

subtype is in the list though?

[Mario Carneiro]

what does "fix it" mean here?

[Mario Carneiro]

(I need to not look at this now, I have to write a presentation)

[Yury G. Kudryashov]

I want to support a custom structure that can't be imported to tactic.auto_cases.

[Yury G. Kudryashov]

(another approach is to rewrite simp lemmas so that they don't expect an U : opens _ to be cased.

[Yury G. Kudryashov]

Probably, I'll try this.

[Reid Barton]

Or can it just stay a subtype?

[Yaël Dillies]

It being a subtype is quite impractical, because we want named projections to extend it.

[Yaël Dillies]

The reasoning might be clearer when looking at docs#topological_space.nonempty_compacts

[Yury G. Kudryashov]

We moved most of other bundled sets to structures (from submonoids to closeds). I think that we should be consistent here.

[Yury G. Kudryashov]

/me is going to prepare for a lecture that starts in <2h