Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat(tactic/dependencies): add tactics to compute (reverse) dependencies #4602

Closed
wants to merge 13 commits into from

Commits on Oct 26, 2020

  1. feat(tactic/dependencies): add tactics to compute (reverse) dependenc…

    …ies of hyps
    
    These are the beginnings of an API about dependencies between expressions. For
    now, we only deal with dependencies and reverse dependencies of hypotheses,
    which are easy to compute.
    
    Breaking change: `tactic.revert_deps` is renamed to
    `tactic.revert_reverse_dependencies_of_hyp` for consistency. Its implementation
    is completely new, but should be equivalent to the old one except for the order
    in which hypotheses are reverted. (But the old implementation made no particular
    guarantees about this order anyway.)
    JLimperg committed Oct 26, 2020
    Copy the full SHA
    08f8668 View commit details
    Browse the repository at this point in the history
  2. Copy the full SHA
    d8a4c23 View commit details
    Browse the repository at this point in the history
  3. Add tests

    JLimperg committed Oct 26, 2020
    Copy the full SHA
    c51ca7f View commit details
    Browse the repository at this point in the history
  4. Placate the linter

    JLimperg committed Oct 26, 2020
    Copy the full SHA
    d68e4b3 View commit details
    Browse the repository at this point in the history
  5. Add variants for list expr, name_set and expr_set for all functions

    I thought these trivial variants would just clutter the API, but then I
    immediately needed a couple of them for another tactic.
    JLimperg committed Oct 26, 2020
    Copy the full SHA
    25ea5bd View commit details
    Browse the repository at this point in the history
  6. Fix type errors

    JLimperg committed Oct 26, 2020
    Copy the full SHA
    e44313d View commit details
    Browse the repository at this point in the history
  7. Copy the full SHA
    87a1e0d View commit details
    Browse the repository at this point in the history
  8. Add doc string

    JLimperg committed Oct 26, 2020
    Copy the full SHA
    b33d5d7 View commit details
    Browse the repository at this point in the history

Commits on Oct 27, 2020

  1. Apply suggestions from code review

    Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
    JLimperg and robertylewis committed Oct 27, 2020
    Copy the full SHA
    d572ac3 View commit details
    Browse the repository at this point in the history
  2. Copy the full SHA
    94c9e03 View commit details
    Browse the repository at this point in the history
  3. Copy the full SHA
    7f89c3e View commit details
    Browse the repository at this point in the history
  4. Copy the full SHA
    c77eac2 View commit details
    Browse the repository at this point in the history

Commits on Oct 28, 2020

  1. Reimplement dependency search; add functions to get dependencies of m…

    …ultiple hyps; improve docs
    JLimperg committed Oct 28, 2020
    Copy the full SHA
    f6f9fad View commit details
    Browse the repository at this point in the history