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.

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

Eliminate the notion of "bound resolution" from inference.md. #4013

Open
wants to merge 2 commits into
base: inference_spec_13
Choose a base branch
from

Commits on Aug 6, 2024

  1. Eliminate the notion of "bound resolution" from inference.md.

    In its place, the spec's definition of "T_0 bounded" is tightened up
    so that for any type T, there is exactly one type T_0 such that T is
    T_0 bounded. Then, instead of saying "let U_0 be the bound resolution
    of T_0", we can say "let U_0 be the unique type such that T_0 is U_0
    bounded."
    
    This avoids some redundancy, since we no longer need to define
    separate but related notions of "T_0 bounded" and "bound resolution".
    stereotype441 committed Aug 6, 2024
    Configuration menu
    Copy the full SHA
    d57c8f9 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    74e5794 View commit details
    Browse the repository at this point in the history