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: propagate Simp.Config when reducing terms and checking definitional equality in simp #6123

Open
wants to merge 17 commits into
base: master
Choose a base branch
from
Open

fix: propagate Simp.Config when reducing terms and checking definitional equality in simp #6123

wants to merge 17 commits into from
+1,130 −59

Commits on Dec 3, 2024

  1. fix: propagate Simp.Config when reducing terms and checking definit… 

    …ional equality in `simp`

This PR ensures that the configuration in `Simp.Config` is used when reducing terms and checking definitional equality in `simp`.

closes #5455

TODO: fix broken tests
    @leodemoura @kim-em
    leodemoura authored and kim-em committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    683aade View commit details
    Browse the repository at this point in the history

  2. chore: add instance Repr Meta.Config

    @leodemoura @kim-em
    leodemoura authored and kim-em committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    7911181 View commit details
    Browse the repository at this point in the history

  3. fix: configuration plumbing in simp

    @leodemoura @kim-em
    leodemoura authored and kim-em committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    9a9cd62 View commit details
    Browse the repository at this point in the history

  4. test: for simp configuration plumbing

    @leodemoura @kim-em
    leodemoura authored and kim-em committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    d77efea View commit details
    Browse the repository at this point in the history

  5. test: make test more robust

    @leodemoura @kim-em
    leodemoura authored and kim-em committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    a1d39cb View commit details
    Browse the repository at this point in the history

  6. chore: fix stage2 issue 

    chore: fix stage2 issues
    @leodemoura @kim-em
    leodemoura authored and kim-em committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    efb15c4 View commit details
    Browse the repository at this point in the history

  7. chore: remove new broken test 

    It has been affected by recent changes to the Std library.
    @leodemoura @kim-em
    leodemoura authored and kim-em committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    79bd075 View commit details
    Browse the repository at this point in the history

  8. fix: Context.setConfig must update metaConfig and indexConfig f… 

    …ields

This PR fixes a bug at `Context.setConfig`. It was not propagating
the configuration to the redundant fields (cache) `metaConfig` and `indexConfig`.
    @leodemoura @kim-em
    leodemoura authored and kim-em committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    ec5be8f View commit details
    Browse the repository at this point in the history

  9. fix: use infer type config when checking types at metavariable assign… 

    …ment

This PR fixes an issue at `isDefEq`. We must use the liberal infer
type `MetaM` config when checking types at the assignment `?m := v`.
    @leodemoura @kim-em
    leodemoura authored and kim-em committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    1e99cdf View commit details
    Browse the repository at this point in the history

  10. test: add split_ifs mwe from Mathlib

    @leodemoura @kim-em
    leodemoura authored and kim-em committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    3570427 View commit details
    Browse the repository at this point in the history

  11. fix: ensure withInferTypeConfig does not override unrelated configu… 

    …ration options
    @leodemoura @kim-em
    leodemoura authored and kim-em committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    3885dfe View commit details
    Browse the repository at this point in the history

  12. chore: remove workaround

    @leodemoura @kim-em
    leodemoura authored and kim-em committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    71b17b6 View commit details
    Browse the repository at this point in the history

  13. test: simp -beta

    @leodemoura @kim-em
    leodemoura authored and kim-em committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    439df9b View commit details
    Browse the repository at this point in the history

  14. add test for mod_cast failure

    @kim-em
    kim-em committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    20e57a1 View commit details
    Browse the repository at this point in the history

  15. chore: add minimization of Mathlib problem from Mathlib.CategoryTheor… 

    …y.Category.Cat.Adjunction
    @kim-em
    kim-em committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    782821a View commit details
    Browse the repository at this point in the history

  16. fix: withInferTypeConfig

    @leodemoura @kim-em
    leodemoura authored and kim-em committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    309dd56 View commit details
    Browse the repository at this point in the history

  17. fix: refine Meta.Config.beta behavior

    @leodemoura @kim-em
    leodemoura authored and kim-em committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    7211be5 View commit details
    Browse the repository at this point in the history