Closed tomaz1502 closed 1 week ago
The goal of this transformation is to bring instances of pattern matching from the goal to the local context.
Note - I am still thinking about which cases of constr we need to consider in the function find_case.
constr
find_case
The goal of this transformation is to bring instances of pattern matching from the goal to the local context.
Note - I am still thinking about which cases of
constrwe need to consider in the functionfind_case.