Zulip Chat Archive

Stream: new members

Topic: term cancelation?


Kasper (Jan 14 2023 at 21:11):

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 (Jan 14 2023 at 22:37):

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

Last updated: Dec 20 2023 at 11:08 UTC