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

fix: make sure refine preserves pre-existing natural mvars #2435

Merged
merged 8 commits into from
Aug 26, 2023
Merged

fix: make sure refine preserves pre-existing natural mvars #2435

merged 8 commits into from
Aug 26, 2023

Commits on Aug 19, 2023

  1. fix: withCollectingNewGoals 

    * don't exclude pre-existing natural mvars
    @thorimur
    thorimur committed Aug 19, 2023
    Configuration menu
    Copy the full SHA
    120022f View commit details
    Browse the repository at this point in the history

  2. test: ensure pre-existing natural mvars are preserved

    @thorimur
    thorimur committed Aug 19, 2023
    Configuration menu
    Copy the full SHA
    d68d2d3 View commit details
    Browse the repository at this point in the history

  3. docs: update comment and include issue number

    @thorimur
    thorimur committed Aug 19, 2023
    Configuration menu
    Copy the full SHA
    35ffec2 View commit details
    Browse the repository at this point in the history

  4. test: expected.out

    @thorimur
    thorimur committed Aug 19, 2023
    Configuration menu
    Copy the full SHA
    9a8d31f View commit details
    Browse the repository at this point in the history

  5. docs: add module docstrings to test 

    * also deleted superfluous `add_synthetic_goal`
    @thorimur
    thorimur committed Aug 19, 2023
    Configuration menu
    Copy the full SHA
    1c813e2 View commit details
    Browse the repository at this point in the history

  6. test: fix expected.out line numbers

    @thorimur
    thorimur committed Aug 19, 2023
    Configuration menu
    Copy the full SHA
    8df381a View commit details
    Browse the repository at this point in the history

Commits on Aug 23, 2023

  1. Update tests/lean/refinePreservesNaturalMVars.lean 

    Co-authored-by: Scott Morrison <scott@tqft.net>
    @thorimur @semorrison
    thorimur and semorrison committed Aug 23, 2023
    Configuration menu
    Copy the full SHA
    ac7b20f View commit details
    Browse the repository at this point in the history

  2. docs: clarify comment

    @thorimur
    thorimur committed Aug 23, 2023
    Configuration menu
    Copy the full SHA
    7a67a32 View commit details
    Browse the repository at this point in the history