a-mir-formality
a-mir-formality copied to clipboard
rust-lang
a model of MIR and the Rust type/trait system
Add `covering set` impl for generic version of trait when all values of a const are covered by impls
When a trait contains a const: i.e. `Foo`, if `T : Foo`, `T: Foo`, we should permit `T : Foo` to be true. This can currently be emulated using specialization...
A counterpart to https://github.com/rust-lang/a-mir-formality/issues/73 enabling negative bounds checking. Currently the impl in the compiler is being reworked to make use of the new trait solver (https://github.com/rust-lang/rust/pull/112875). Despite the feature being...
Per [this conversation](https://rust-lang.zulipchat.com/#narrow/stream/326132-t-types.2Fmeetings/topic/2022-10-21.20issue.20triage/near/305357001), we should model: * rust-lang/rust#84533 * rust-lang/rust#84591 * rust-lang/rust#98117
The description of `crate-item-ok-goal` for function declarations specifies that > For a fn declaration declared in the crate C, like the following: > > fn foo u32 where T: Ord...
Decls debug rendering is a bit noisy, especially since decls does not change, but is printed for every step that failed. With this change, decls is only printed in the...
`formality-check` isn't rejecting an is-implemented where clause with nonsense in the implementing type or in a parameter to the trait. For example it doesn't reject a where clause whose implementing...
This change adds a syntax for specifying FnDefs and FnPtrs as type parameters, `fn name` and `fn(T, U,...) -> V` respectively. The `fn` prefix is used to disambiguate between adt...
This is pretty crude. We generate garbage and we don't even run tests because it's not really good enough to be useful. But I figured the basic setup makes sense...
Currently, the names of the matched rules are displayed in certain paths, prominently when there is an error or constraints are produced. This PR displays the names of the rules...
the current solver when encountering ambiguity during proving should consider reproving if progress has been made