You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
addProof(newLKIncomplete(awaitmodalSequentPrompt('Enter an LK goal sequent:')))
@@ -335,6 +343,9 @@ You can click on the <span style="color: ${incompleteColor}">orange</span> sciss
335
343
</p>
336
344
<p>
337
345
For rules with premises, you can click on the <span style="background: ${foldColor}">gray</span> hide button (⃠) to hide the premises of a proof rule, which shows each premise as an ellipses. Clicking the same button again will reveal the premises. You can use this feature to clean up your workspace while working on large proofs.
346
+
</p>
347
+
<p>
348
+
The left bar contains a list of proofs you are working on at a given time. You can click on the goal to select the proof tree in the workspace. Double clicking on the goal will pan you to the proof tree, and reset the zoom. The icon next to buttons for each proof shows whether you have finished the proof (<span class="resultOk">✓</span> or <span class="resultOk">✓*</span> if you have used Z3), or still working on your proof (<span class="resultIncomplete" title="Incomplete proof">✎</span>), or whether the proof has failed for some subtree (<span class="resultBad" title="A part of this proof has failed">✖</span>).
338
349
</p>
339
350
<p>
340
351
As you work on the proof, you can click on the buttons on the left bar to either copy the <span class="latex">L<sup>a</sup>T<sub>e</sub>X</span> output for a given proof, or to save that proof onto your computer as a file. You can later reload the proof file into the proof assistant by clicking the "Load proof file" button on the top bar.
0 commit comments