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] - refactor(Mathport): move mathport prelude to mathlib4 #80

Closed
wants to merge 25 commits into from
Closed

[Merged by Bors] - refactor(Mathport): move mathport prelude to mathlib4 #80

wants to merge 25 commits into from

Commits on Oct 26, 2021

  1. refactor(Mathport): move mathport prelude to mathlib4

    @semorrison
    semorrison committed Oct 26, 2021
    Configuration menu
    Copy the full SHA
    64a65f5 View commit details
    Browse the repository at this point in the history

  2. fix CI

    @semorrison
    semorrison committed Oct 26, 2021
    Configuration menu
    Copy the full SHA
    083fcbb View commit details
    Browse the repository at this point in the history

  3. update README

    @semorrison
    semorrison committed Oct 26, 2021
    Configuration menu
    Copy the full SHA
    69a7ac0 View commit details
    Browse the repository at this point in the history

  4. add imports, remove syntaxes

    @semorrison
    semorrison committed Oct 26, 2021
    Configuration menu
    Copy the full SHA
    0a4c17d View commit details
    Browse the repository at this point in the history

  5. more comments

    @semorrison
    semorrison committed Oct 26, 2021
    Configuration menu
    Copy the full SHA
    5a3428e View commit details
    Browse the repository at this point in the history

Commits on Oct 27, 2021

  1. move rcases patterns, put comment in Tactic/Ext about mismatch

    @semorrison
    semorrison committed Oct 27, 2021
    Configuration menu
    Copy the full SHA
    acdd4f5 View commit details
    Browse the repository at this point in the history

  2. adjust syntax for showTerm

    @semorrison
    semorrison committed Oct 27, 2021
    Configuration menu
    Copy the full SHA
    890b593 View commit details
    Browse the repository at this point in the history

  3. librarySearch

    @semorrison
    semorrison committed Oct 27, 2021
    Configuration menu
    Copy the full SHA
    dbbb2bd View commit details
    Browse the repository at this point in the history

Commits on Nov 1, 2021

  1. comments

    @semorrison
    semorrison committed Nov 1, 2021
    Configuration menu
    Copy the full SHA
    7cd174a View commit details
    Browse the repository at this point in the history

  2. remove duplicate syntax for showTerm, and add name to the elab command

    @semorrison
    semorrison committed Nov 1, 2021
    Configuration menu
    Copy the full SHA
    a58ce88 View commit details
    Browse the repository at this point in the history

  3. update Mathlib.lean

    @semorrison
    semorrison committed Nov 1, 2021
    Configuration menu
    Copy the full SHA
    0642488 View commit details
    Browse the repository at this point in the history

  4. breaking normNum

    @semorrison
    semorrison committed Nov 1, 2021
    Configuration menu
    Copy the full SHA
    2d9b704 View commit details
    Browse the repository at this point in the history

  5. still broken

    @semorrison
    semorrison committed Nov 1, 2021
    Configuration menu
    Copy the full SHA
    41b423a View commit details
    Browse the repository at this point in the history

  6. uncomment import_private syntax, fix comment

    @semorrison
    semorrison committed Nov 1, 2021
    Configuration menu
    Copy the full SHA
    1542d19 View commit details
    Browse the repository at this point in the history

  7. break solveByElim, too

    @semorrison
    semorrison committed Nov 1, 2021
    Configuration menu
    Copy the full SHA
    5f9e620 View commit details
    Browse the repository at this point in the history

  8. use elab_rules in librarySearch

    @semorrison
    semorrison committed Nov 1, 2021
    Configuration menu
    Copy the full SHA
    acb2824 View commit details
    Browse the repository at this point in the history

Commits on Nov 3, 2021

  1. explicitly use syntax category in elab_rules matches

    @semorrison
    semorrison committed Nov 3, 2021
    Configuration menu
    Copy the full SHA
    0bc26be View commit details
    Browse the repository at this point in the history

  2. comments

    @semorrison
    semorrison committed Nov 3, 2021
    Configuration menu
    Copy the full SHA
    df3daea View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/master' into migrate_mathport_pr… 

    …elude
    @semorrison
    semorrison committed Nov 3, 2021
    Configuration menu
    Copy the full SHA
    56203de View commit details
    Browse the repository at this point in the history

Commits on Nov 8, 2021

  1. Merge remote-tracking branch 'origin/master' into migrate_mathport_pr… 

    …elude
    @semorrison
    semorrison committed Nov 8, 2021
    Configuration menu
    Copy the full SHA
    3e164f1 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/Mathport/Syntax.lean 

    Co-authored-by: Gabriel Ebner <gebner@gebner.org>
    @semorrison @gebner
    semorrison and gebner committed Nov 8, 2021
    Configuration menu
    Copy the full SHA
    2e0cf16 View commit details
    Browse the repository at this point in the history

  3. guard*

    @semorrison
    semorrison committed Nov 8, 2021
    Configuration menu
    Copy the full SHA
    3f266e5 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'migrate_mathport_prelude' of github.com:leanprover-comm… 

    …unity/mathlib4 into migrate_mathport_prelude
    @semorrison
    semorrison committed Nov 8, 2021
    Configuration menu
    Copy the full SHA
    7627b87 View commit details
    Browse the repository at this point in the history

  5. fix tests

    @semorrison
    semorrison committed Nov 8, 2021
    Configuration menu
    Copy the full SHA
    8d124cf View commit details
    Browse the repository at this point in the history

  6. fix test

    @semorrison
    semorrison committed Nov 8, 2021
    Configuration menu
    Copy the full SHA
    26faef7 View commit details
    Browse the repository at this point in the history