Use hypotheses when doing compile_match
For the following example:
use list.List
constant l: list int = Cons 42 Nil
goal G : 42 = match l with Nil -> 0 | Cons x _ -> x end
if I want to get a goal of the form 42 = 42
, I must do first subst_all
and only then compile_match
is able to give me 42 = 42
.
Would it be possible for compile_match
to use hypotheses of the form H: e = e'
to further simplify goals of the form match e with e' -> ... end
?