Code

Prettyprint/produce proof tree#43

Code

Open

nishantjr wants to merge 7 commits intomasterkframework/matching-logic-prover:masterfrom detailed-proofskframework/matching-logic-prover:detailed-proofsCopy head branch name to clipboard

+137-14

Commits

Commits on Apr 22, 2020

• core: Sequential composition uses subgoals too

  nishantjr

  committed
  7bac10e

  Copy full SHA for 7bac10e

• Reap failed goals and children (TODO: This uses [owise])

  nishantjr

  committed
  018f0f2

  Copy full SHA for 018f0f2

• lib/render-proof-tree: Small python script for extracting tree structure

  nishantjr

  committed
  ec54f36

  Copy full SHA for ec54f36

• strategies/core: Do not copy the trace to subgoals

  Show description for 146e6ee
  nishantjr

  committed
  146e6ee

  Copy full SHA for 146e6ee

• strategies/smt: Place SMTLIB2Script in trace cell

  nishantjr

  committed
  8ea3877

  Copy full SHA for 8ea3877

• lib/render-proof-tree: Prints prints current goal, and trace cells

  nishantjr

  committed
  54c0285

  Copy full SHA for 54c0285

• core: cool sequences back in, so that subgoals are only generated for a single uncomposed strategy

  nishantjr

  committed
  e1dd33a

  Copy full SHA for e1dd33a