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

feat: Add some theorems for String.substrEq and String.isPrefixOf #782

Closed
wants to merge 8 commits into from
Closed

feat: Add some theorems for String.substrEq and String.isPrefixOf #782

wants to merge 8 commits into from

Commits on May 6, 2024

  1. Add lemmas necessary for isPrefixOf proofs 

    - `String.cons_append`
- `String.Pos.empty_valid`
- `String.Pos.Valid.cons_addChar`
- `String.Pos.Valid.cons_zero_or_ge_head`

Update Lemmas.lean

Update Lemmas.lean
    @tjf801
    tjf801 committed May 6, 2024
    Configuration menu
    Copy the full SHA
    0489657 View commit details
    Browse the repository at this point in the history

  2. Add isPrefixOf proofs

    @tjf801
    tjf801 committed May 6, 2024
    Configuration menu
    Copy the full SHA
    b4afe21 View commit details
    Browse the repository at this point in the history

Commits on May 13, 2024

  1. add info about unusedHavesSuffices lint 

    Co-authored-by: Kim Morrison <kim@tqft.net>
    @tjf801 @semorrison
    tjf801 and semorrison committed May 13, 2024
    Configuration menu
    Copy the full SHA
    b0ac67f View commit details
    Browse the repository at this point in the history

  2. remove unnecessary data_append theorem

    @tjf801
    tjf801 committed May 13, 2024
    Configuration menu
    Copy the full SHA
    9c1bf76 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'main' into isPrefixOf-theorems

    @tjf801
    tjf801 committed May 13, 2024
    Configuration menu
    Copy the full SHA
    10a27cc View commit details
    Browse the repository at this point in the history

  4. Revert "remove unnecessary data_append theorem" 

    This reverts commit 9c1bf76.
    @tjf801
    tjf801 committed May 13, 2024
    Configuration menu
    Copy the full SHA
    cc2174d View commit details
    Browse the repository at this point in the history

  5. make cons_append not @[simp]

    @tjf801
    tjf801 committed May 13, 2024
    Configuration menu
    Copy the full SHA
    c7d6250 View commit details
    Browse the repository at this point in the history

Commits on May 18, 2024

  1. Merge branch 'leanprover-community:main' into isPrefixOf-theorems

    @tjf801
    tjf801 committed May 18, 2024
    Configuration menu
    Copy the full SHA
    8895e19 View commit details
    Browse the repository at this point in the history