`cases` builder should accept type synonyms

leanprover-community / aesop

White-box automation for Lean 4

Apache License 2.0

157 stars 25 forks source link

`cases` builder should accept type synonyms #46

Closed JLimperg closed 1 year ago

JLimperg commented 1 year ago

attribute [aesop safe cases] C where C := Option Nat should be legal. Currently, the cases builder complains that C is not an inductive type.

JLimperg commented 1 year ago

This is actually more effort than I thought since we would need to adjust the indexing and patterns option as well. So wontfix. If this ever gets reopened, make sure that constructor gets symmetric treatment.