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(library/init/coe): backport has_coe_to_sort/has_coe_to_fun from Lean 4 #557

Closed
wants to merge 19 commits into from
Closed

[Merged by Bors] - feat(library/init/coe): backport has_coe_to_sort/has_coe_to_fun from Lean 4 #557

wants to merge 19 commits into from

Commits on Mar 18, 2021

  1. library/init/coe compiles with the new has_coe_to_sort/`has_coe_t… 

    …o_fun`
    @urkud
    urkud committed Mar 18, 2021
    Configuration menu
    Copy the full SHA
    3ebd4dd View commit details
    Browse the repository at this point in the history

  2. Fix number of coercion arguments.

    @gebner
    gebner committed Mar 18, 2021
    Configuration menu
    Copy the full SHA
    0ed322e View commit details
    Browse the repository at this point in the history

  3. Fix library/ and some tests

    @urkud
    urkud committed Mar 18, 2021
    Configuration menu
    Copy the full SHA
    428317f View commit details
    Browse the repository at this point in the history

  4. Change instance naming heuristic.

    @gebner
    gebner committed Mar 18, 2021
    Configuration menu
    Copy the full SHA
    b504d92 View commit details
    Browse the repository at this point in the history

  5. Fix coe pp.

    @gebner
    gebner committed Mar 18, 2021
    Configuration menu
    Copy the full SHA
    f694655 View commit details
    Browse the repository at this point in the history

  6. Change instance heuristic some more.

    @gebner
    gebner committed Mar 18, 2021
    Configuration menu
    Copy the full SHA
    44c0d37 View commit details
    Browse the repository at this point in the history

  7. Fix some tests.

    @gebner
    gebner committed Mar 18, 2021
    Configuration menu
    Copy the full SHA
    6b51a52 View commit details
    Browse the repository at this point in the history

  8. Revert "Change instance heuristic some more." 

    This reverts commit 44c0d37.
    @gebner
    gebner committed Mar 18, 2021
    Configuration menu
    Copy the full SHA
    c711136 View commit details
    Browse the repository at this point in the history

  9. Fix some tests.

    @gebner
    gebner committed Mar 18, 2021
    Configuration menu
    Copy the full SHA
    744be00 View commit details
    Browse the repository at this point in the history

  10. Fix one more test.

    @gebner
    gebner committed Mar 18, 2021
    Configuration menu
    Copy the full SHA
    b8b2426 View commit details
    Browse the repository at this point in the history

Commits on Mar 19, 2021

  1. Tweak instance naming.

    @gebner
    gebner committed Mar 19, 2021
    3 Configuration menu
    Copy the full SHA
    6542984 View commit details
    Browse the repository at this point in the history

  2. Fix tests.

    @gebner
    gebner committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    d2f2df8 View commit details
    Browse the repository at this point in the history

  3. Remove unnecessary instance names.

    @gebner
    gebner committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    da53b38 View commit details
    Browse the repository at this point in the history

  4. Add todo.

    @gebner
    gebner committed Mar 19, 2021
    Configuration menu
    Copy the full SHA
    deb0946 View commit details
    Browse the repository at this point in the history

Commits on Mar 26, 2021

  1. Synthesize tc insts before anon cstrs.

    @gebner
    gebner committed Mar 26, 2021
    Configuration menu
    Copy the full SHA
    f116eaf View commit details
    Browse the repository at this point in the history

Commits on Sep 11, 2021

  1. Merge branch 'master' into coe-fn-backport

    @urkud
    urkud committed Sep 11, 2021
    Configuration menu
    Copy the full SHA
    e4342cc View commit details
    Browse the repository at this point in the history

Commits on Sep 12, 2021

  1. Fix conflict with mathlib

    @urkud
    urkud committed Sep 12, 2021
    Configuration menu
    Copy the full SHA
    dcc4426 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'LO-fix' into coe-fn-backport

    @urkud
    urkud committed Sep 12, 2021
    Configuration menu
    Copy the full SHA
    d09b2a8 View commit details
    Browse the repository at this point in the history

Commits on Sep 17, 2021

  1. Merge branch 'master' into coe-fn-backport

    @urkud
    urkud committed Sep 17, 2021
    Configuration menu
    Copy the full SHA
    51a0a55 View commit details
    Browse the repository at this point in the history