[isabelle] case-expression and simplification
is there any deeper reason why abbreviations do not work with "case _
of" - expressions?
On the other side, they work well with case-splitting in the
datatype test = A "nat list" | B
abbreviation "As n == A [n]"
fun f where "f (As n) = True" | "f _ = False" (* Works well! *)
lemma "(case x of As n => n | _ => 0) = 0" (* Does not work! *)
This archive was generated by a fusion of
Pipermail (Mailman edition) and