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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - fix(init/meta/converter/interactive): Do not ignore errors and tactic state changes in for and find #482

Closed
wants to merge 21 commits into from
Closed

[Merged by Bors] - fix(init/meta/converter/interactive): Do not ignore errors and tactic state changes in for and find #482

wants to merge 21 commits into from

Commits on Oct 8, 2020

  1. fix(init/meta/converter/interactive): Do not ignore errors in for

    @eric-wieser
    eric-wieser committed Oct 8, 2020
    Configuration menu
    Copy the full SHA
    fef512c View commit details
    Browse the repository at this point in the history

  2. chore(*): Add a test for for with typos in conv mode

    @eric-wieser
    eric-wieser committed Oct 8, 2020
    Configuration menu
    Copy the full SHA
    c111719 View commit details
    Browse the repository at this point in the history

  3. fix(*): Missing namespace

    @eric-wieser
    eric-wieser committed Oct 8, 2020
    Configuration menu
    Copy the full SHA
    a098e5d View commit details
    Browse the repository at this point in the history

Commits on Oct 9, 2020

  1. fix(*): Add comments, fix state, fix imports

    @eric-wieser
    eric-wieser committed Oct 9, 2020
    Configuration menu
    Copy the full SHA
    dac2cf6 View commit details
    Browse the repository at this point in the history

  2. fix(*): typo

    @eric-wieser
    eric-wieser committed Oct 9, 2020
    Configuration menu
    Copy the full SHA
    9949579 View commit details
    Browse the repository at this point in the history

  3. Update interactive.lean

    @eric-wieser
    eric-wieser committed Oct 9, 2020
    Configuration menu
    Copy the full SHA
    9e720b9 View commit details
    Browse the repository at this point in the history

  4. feat(init/meta/tactic): capture and unwrap

    @eric-wieser
    eric-wieser committed Oct 9, 2020
    Configuration menu
    Copy the full SHA
    67065b2 View commit details
    Browse the repository at this point in the history

  5. fix(meta/converter/interactive): Cleanup and fix find too

    @eric-wieser
    eric-wieser committed Oct 9, 2020
    Configuration menu
    Copy the full SHA
    1c65270 View commit details
    Browse the repository at this point in the history

  6. Update tactic.lean

    @eric-wieser
    eric-wieser committed Oct 9, 2020
    Configuration menu
    Copy the full SHA
    aa5edea View commit details
    Browse the repository at this point in the history

  7. Update tactic.lean

    @eric-wieser
    eric-wieser committed Oct 9, 2020
    Configuration menu
    Copy the full SHA
    3afbf71 View commit details
    Browse the repository at this point in the history

  8. fix(*): Undo t <$> read which doesn't work

    @eric-wieser
    eric-wieser committed Oct 9, 2020
    Configuration menu
    Copy the full SHA
    42debdb View commit details
    Browse the repository at this point in the history

  9. fix(*): Fix namespacing

    @eric-wieser
    eric-wieser committed Oct 9, 2020
    Configuration menu
    Copy the full SHA
    72587c3 View commit details
    Browse the repository at this point in the history

  10. doc(*): Describe the limitations of ext_simplify_core

    @eric-wieser
    eric-wieser committed Oct 9, 2020
    Configuration menu
    Copy the full SHA
    c562e35 View commit details
    Browse the repository at this point in the history

Commits on Oct 10, 2020

  1. refactor(*): Replace a match with an unwrap

    @eric-wieser
    eric-wieser committed Oct 10, 2020
    Configuration menu
    Copy the full SHA
    fc9da45 View commit details
    Browse the repository at this point in the history

Commits on Oct 12, 2020

  1. Update tactic.lean

    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    e7f4330 View commit details
    Browse the repository at this point in the history

  2. Update tactic.lean

    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    e16bae1 View commit details
    Browse the repository at this point in the history

  3. Update simp_tactic.lean

    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    b8f2963 View commit details
    Browse the repository at this point in the history

  4. Update interactive.lean

    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    f11aaec View commit details
    Browse the repository at this point in the history

  5. Update tests

    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    3e0b4d9 View commit details
    Browse the repository at this point in the history

  6. Create conv_for_find.lean.expected.out

    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    0315acb View commit details
    Browse the repository at this point in the history

  7. Update conv_for_find.lean.expected.out

    @eric-wieser
    eric-wieser committed Oct 12, 2020
    Configuration menu
    Copy the full SHA
    934d83d View commit details
    Browse the repository at this point in the history