mirror of
https://github.com/astral-sh/ruff.git
synced 2025-10-01 22:31:47 +00:00
[red-knot] 'is_equivalent_to' is an equivalence relation (#15488)
## Summary Adds two additional tests for `is_equivalent_to` so that we cover all properties of an [equivalence relation]. ## Test Plan ``` while cargo test --release -p red_knot_python_semantic -- --ignored types::property_tests::stable; do :; done ``` [equivalence relation]: https://en.wikipedia.org/wiki/Equivalence_relation
This commit is contained in:
parent
96c2d0996d
commit
d4862844f1
1 changed files with 15 additions and 2 deletions
|
@ -234,12 +234,25 @@ mod stable {
|
|||
use super::union;
|
||||
use crate::types::{KnownClass, Type};
|
||||
|
||||
// `T` is equivalent to itself.
|
||||
// Reflexivity: `T` is equivalent to itself.
|
||||
type_property_test!(
|
||||
equivalent_to_is_reflexive, db,
|
||||
forall types t. t.is_fully_static(db) => t.is_equivalent_to(db, t)
|
||||
);
|
||||
|
||||
// Symmetry: If `S` is equivalent to `T`, then `T` must be equivalent to `S`.
|
||||
// Note that this (trivially) holds true for gradual types as well.
|
||||
type_property_test!(
|
||||
equivalent_to_is_symmetric, db,
|
||||
forall types s, t. s.is_equivalent_to(db, t) => t.is_equivalent_to(db, s)
|
||||
);
|
||||
|
||||
// Transitivity: If `S` is equivalent to `T` and `T` is equivalent to `U`, then `S` must be equivalent to `U`.
|
||||
type_property_test!(
|
||||
equivalent_to_is_transitive, db,
|
||||
forall types s, t, u. s.is_equivalent_to(db, t) && t.is_equivalent_to(db, u) => s.is_equivalent_to(db, u)
|
||||
);
|
||||
|
||||
// A fully static type `T` is a subtype of itself.
|
||||
type_property_test!(
|
||||
subtype_of_is_reflexive, db,
|
||||
|
@ -365,7 +378,7 @@ mod flaky {
|
|||
|
||||
// For two fully static types, their intersection must be a subtype of each type in the pair.
|
||||
type_property_test!(
|
||||
all_fully_static_type_pairs_are_supertypes_of_their_union, db,
|
||||
all_fully_static_type_pairs_are_supertypes_of_their_intersection, db,
|
||||
forall types s, t.
|
||||
s.is_fully_static(db) && t.is_fully_static(db)
|
||||
=> intersection(db, s, t).is_subtype_of(db, s) && intersection(db, s, t).is_subtype_of(db, t)
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue