Traits for transforming bits of IR.
Useful macros for writing unit tests. They let you gin up dummy types and things.
Indicates that the
Wraps a "canonicalized item". Items are canonicalized as follows:
Combines a substitution (
The set of assumptions we've made so far, and the current number of universal (forall) quantifiers we're within.
Proves that the given projection normalizes to the given
type. A projection
Index of an universally quantified parameter in the environment. Two indexes are required, the one of the universe itself and the relative index inside the universe.
Represents one clause of the form
Proves equality between a projection
for<'a...'z> X -- all binders are instantiated at once,
and we use deBruijn indices within
A mapping of inference variables to instantiations thereof.
A "universe canonical" value. This is a wrapper around a
An universe index is how a universally quantified parameter is
represented when it's binder is moved into the environment.
An example chain of transformations would be:
Indicates that the trait where the associated type belongs to is
not yet known, i.e. is unselected. For example, a normal
A constraint on lifetimes.
A "domain goal" is a goal that is directly about Rust, rather than a pure logical statement. As much as possible, the Chalk solver should avoid decomposing this enum, and instead treat its values opaquely.
A general goal; this is the full range of questions you can pose to Chalk.
A goal that does not involve any logical connectives. Equality is treated specially by the logic (as with most first-order logics), since it interacts with unification etc.
Where clauses that can be written by a Rust programmer.