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] - feat: port field_simp tactic #1824

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - feat: port field_simp tactic #1824

wants to merge 9 commits into from

Commits on Jan 24, 2023

  1. feat: port field_simp tactic

    @dwrensha
    dwrensha committed Jan 24, 2023
    Configuration menu
    Copy the full SHA
    b5bd20d View commit details
    Browse the repository at this point in the history

Commits on Jan 27, 2023

  1. Merge branch 'master' into field_simp

    @dwrensha
    dwrensha committed Jan 27, 2023
    Configuration menu
    Copy the full SHA
    410d205 View commit details
    Browse the repository at this point in the history

  2. remove needless 'pure ()'

    @dwrensha
    dwrensha committed Jan 27, 2023
    Configuration menu
    Copy the full SHA
    7d38c65 View commit details
    Browse the repository at this point in the history

  3. uncomment field_simp examples in test/ring.lean, and get them to work

    @dwrensha
    dwrensha committed Jan 27, 2023
    Configuration menu
    Copy the full SHA
    52bb68c View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' into field_simp

    @dwrensha
    dwrensha committed Jan 27, 2023
    Configuration menu
    Copy the full SHA
    dac6bbb View commit details
    Browse the repository at this point in the history

  5. fix merge conflict

    @dwrensha
    dwrensha committed Jan 27, 2023
    Configuration menu
    Copy the full SHA
    4972598 View commit details
    Browse the repository at this point in the history

Commits on Jan 28, 2023

  1. Merge branch 'master' into field_simp

    @dwrensha
    dwrensha committed Jan 28, 2023
    Configuration menu
    Copy the full SHA
    ace00b0 View commit details
    Browse the repository at this point in the history

Commits on Feb 6, 2023

  1. Merge branch 'master' into field_simp

    @dwrensha
    dwrensha committed Feb 6, 2023
    Configuration menu
    Copy the full SHA
    0a93582 View commit details
    Browse the repository at this point in the history

Commits on Feb 10, 2023

  1. Merge branch 'master' into field_simp

    @dwrensha
    dwrensha committed Feb 10, 2023
    Configuration menu
    Copy the full SHA
    9cf9beb View commit details
    Browse the repository at this point in the history