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 Data.Nat.Count #2209

Closed
wants to merge 35 commits into from
Closed

[Merged by Bors] - feat: port Data.Nat.Count #2209

wants to merge 35 commits into from

Commits on Feb 7, 2023

  1. start: create files

    @thorimur
    thorimur committed Feb 7, 2023
    Configuration menu
    Copy the full SHA
    10e70e6 View commit details
    Browse the repository at this point in the history

  2. chore: update Mathlib.lean

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

Commits on Feb 8, 2023

  1. test: port mathlib3 tests

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

Commits on Feb 9, 2023

  1. feat: add getFVarId(s)At to Tactic.Core 

    * handles case where we want goal.withContext instead of withMainContext
    @thorimur
    thorimur committed Feb 9, 2023
    Configuration menu
    Copy the full SHA
    7af8d0f View commit details
    Browse the repository at this point in the history

  2. feat: wlog tactic

    @thorimur
    thorimur committed Feb 9, 2023
    Configuration menu
    Copy the full SHA
    8c4c561 View commit details
    Browse the repository at this point in the history

  3. test: update tests

    @thorimur
    thorimur committed Feb 9, 2023
    Configuration menu
    Copy the full SHA
    990d5e3 View commit details
    Browse the repository at this point in the history

  4. chore: update syntax to match mathport 

    Co-authored-by: Mario Carneiro <di.gama@gmail.com>
    @thorimur @digama0
    thorimur and digama0 committed Feb 9, 2023
    Configuration menu
    Copy the full SHA
    bfa50ff View commit details
    Browse the repository at this point in the history

  5. test: fix this

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

Commits on Feb 10, 2023

  1. Update Mathlib/Tactic/WLOG.lean

    @mcdoll
    mcdoll committed Feb 10, 2023
    Configuration menu
    Copy the full SHA
    9566c55 View commit details
    Browse the repository at this point in the history

  2. added a test

    @mcdoll
    mcdoll committed Feb 10, 2023
    Configuration menu
    Copy the full SHA
    52ae9e1 View commit details
    Browse the repository at this point in the history

  3. feat: broaden capabilities of getFVarIdsAt

    @thorimur
    thorimur committed Feb 10, 2023
    Configuration menu
    Copy the full SHA
    3b4af71 View commit details
    Browse the repository at this point in the history

  4. refactor: create definition wlog for goal.wlog 

    * keep track of fvarid output in keeping with `intro`/`byCases`/etc.
    @thorimur
    thorimur committed Feb 10, 2023
    Configuration menu
    Copy the full SHA
    523a4cd View commit details
    Browse the repository at this point in the history

  5. test: expand tests a little

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

  6. chore: minor cleanups

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

  7. fix: getFVarIdsAt (overzealous return)

    @thorimur
    thorimur committed Feb 10, 2023
    Configuration menu
    Copy the full SHA
    04f0c4b View commit details
    Browse the repository at this point in the history

Commits on Feb 11, 2023

  1. chore: minor rename

    @thorimur
    thorimur committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    beee187 View commit details
    Browse the repository at this point in the history

  2. chore: remove stray set_option from test

    @thorimur
    thorimur committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    77ccd77 View commit details
    Browse the repository at this point in the history

  3. feat: account for _ in binderIdent

    @thorimur
    thorimur committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    bf75e67 View commit details
    Browse the repository at this point in the history

  4. test: test _ in binderIdent

    @thorimur
    thorimur committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    c824a93 View commit details
    Browse the repository at this point in the history

  5. docs: minor fixes

    @thorimur
    thorimur committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    c05d0b4 View commit details
    Browse the repository at this point in the history

  6. fix: broaden to impl. details in getFVarIdsAt 

    * make default
    @thorimur
    thorimur committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    acc8562 View commit details
    Browse the repository at this point in the history

  7. refactor: filterOutImplementationDetails in Core

    @thorimur
    thorimur committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    caebdee View commit details
    Browse the repository at this point in the history

  8. refactor: pull plumbing out of revert & assert

    @thorimur
    thorimur committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    0df245a View commit details
    Browse the repository at this point in the history

  9. feat: port Data.Nat.Count

    @xroblot
    xroblot committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    296eb96 View commit details
    Browse the repository at this point in the history

  10. Initial file copy from mathport

    @xroblot
    xroblot committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    5111be7 View commit details
    Browse the repository at this point in the history

  11. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @xroblot
    xroblot committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    dd4b867 View commit details
    Browse the repository at this point in the history

  12. 1st pass

    @xroblot
    xroblot committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    0f42d5e View commit details
    Browse the repository at this point in the history

  13. auto: naming

    @xroblot
    xroblot committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    f073c8e View commit details
    Browse the repository at this point in the history

  14. refactor: use withFreshCache

    @thorimur
    thorimur committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    0d640c8 View commit details
    Browse the repository at this point in the history

  15. wlog needed

    @xroblot
    xroblot committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    873cd8e View commit details
    Browse the repository at this point in the history

  16. Merge remote-tracking branch 'origin/wlog' into port/Data.Nat.Count

    @xroblot
    xroblot committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    c4f86d7 View commit details
    Browse the repository at this point in the history

  17. Merge with wlog

    @xroblot
    xroblot committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    51f62d6 View commit details
    Browse the repository at this point in the history

Commits on Feb 13, 2023

  1. Merge remote-tracking branch 'origin' into port/Data.Nat.Count

    @xroblot
    xroblot committed Feb 13, 2023
    Configuration menu
    Copy the full SHA
    25a284f View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into port/Data.Nat.Count

    @xroblot
    xroblot committed Feb 13, 2023
    Configuration menu
    Copy the full SHA
    384d4e9 View commit details
    Browse the repository at this point in the history

Commits on Feb 14, 2023

  1. Fixed scoped

    @xroblot
    xroblot committed Feb 14, 2023
    Configuration menu
    Copy the full SHA
    2308e11 View commit details
    Browse the repository at this point in the history