search

kframework / matching-logic-prover

15 stars 4 forks source link

Fix Kore driver #67

Closed h0nzZik closed 4 years ago

h0nzZik commented 4 years ago
  1. the subgoal strategy belongs to the <strategy> cell
  2. keep the goal containing the <k> cell with the declarations on top of the list of all proven goals, so that it can be used process nother declarations after proving the goal - thus supporting multiple goals in a file.
nishantjr commented 4 years ago

I realized I made a mistake: The claim cell should have remained unchanged and the <strategy> cell should have been merged with <k> that would remove the need for the goalUp strategy you've implemented here. Sorry about that

h0nzZik commented 4 years ago

@nishantjr even in that case, we would still need the goalUp strategy, since we cannot match deeper in the list - or is the Cell handled differently?