小编502*_*32E的帖子

当对cases归纳数据类型使用 - 策略时，精益会生成多个案例，但不会创建说明当前案例假设的假设。例如：

inductive color | blue | red\n\ntheorem exmpl (c : color) : true :=\nbegin\n    cases c,\nend\n

导致以下战术状态

case color.blue\n\xe2\x8a\xa2 true\ncase color.red\n\xe2\x8a\xa2 true\n

但没有创建一个单独的假设（如c = color.red）来使用。你如何得到这样的假设？