term cancelation?

Stream: new members

[Kasper]

Hey guys.

I have a question.
I have the following hypothesis: h: solver._match_1 (find_valuation (form.FAnd p1 p2)) = tt

My goal is the following: solver._match_1 (find_valuation p1) = tt

Two questions:

1. as you can see from the hypothesis and the goal, their form is very similar. In fact both are solver.match_1 ... = tt. Is there a way to get rid of these terms? So I end up with a hypothesis of find_valuation (form.FAnd p1 p2) and a goal of find_valuation p1 or am I saying something ridiculous?

2. I see the term _match_1. I assume this is introduced by a pattern match I perform in the solver definition. What exactly does this do?

[Alex J. Best]

A #mwe would be helpful so we can give better advice for your exact situation.

1. it sounds like you are asking for tactic#convert maybe?
2. its a little strange that you are seeing that in the first place, and makes me think you unfolded your definitions too much already