GitLab

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 ?