Skip to content
This repository has been archived by the owner on Aug 2, 2024. It is now read-only.

proof improvements #136

Open
5 of 6 tasks
thevirtuoso1973 opened this issue Feb 17, 2022 · 1 comment
Open
5 of 6 tasks

proof improvements #136

thevirtuoso1973 opened this issue Feb 17, 2022 · 1 comment
Assignees

Comments

@thevirtuoso1973
Copy link
Contributor

thevirtuoso1973 commented Feb 17, 2022

  • More consistent interface with build
  • Don't rely on colour as much, since users may have their own term colour settings that won't match.
  • Highlight image predicates.
  • Option to omit resolution steps
  • Collapse operator applications. e.g. cases like
    (
      (
        ...
      )::op1
    )::op2
    
  • Nicer run formatting. Might need a different proof tree printer however. Ideally it would be 'newline aware', where it will correctly indent newlines.
@thevirtuoso1973 thevirtuoso1973 changed the title Proof improvements proof improvements Feb 17, 2022
@thevirtuoso1973 thevirtuoso1973 self-assigned this Feb 17, 2022
@thevirtuoso1973
Copy link
Contributor Author

thevirtuoso1973 commented Apr 7, 2022

Would be pretty useful to diff proof trees as a regression test method.
E.g. your CI/build system can print out tree diffs as a warning for any new commits.

Not sure how best to actually implement though. Could start with just a simple text differ and somehow integrate from there.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant