You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
It must be possible, when specifying methods, to refer to the type that the interface is implemented on. For example, an add method on iface num, which takes an extra parameter of the same type and returns a value of the same type, can't be expressed in the current system without adding a lot of noisy type parameters.
iface num {
fn add(x: self) -> self;
fn sub(x: self) -> self;
/* etc */
}
impl of num for int {
fn add(x: int) -> int { self + x }
fn sub(x: int) -> int { self - x }
}
The self type is an implicit type parameter refers to the specialized type. An interface that uses it can not be cast to, since it'd be impossible to type its methods in the absence of a concrete self type.
The text was updated successfully, but these errors were encountered:
So the way this ended up working, internally, is somewhat kludgy, which suggests it might not be the most well-designed feature. Constructive feedback welcome.
…unctions (rust-lang#1661)
Instead of having to manually wrap the code in `kani::spawnable_block_on` as in rust-lang#1659, this PR allows `#[kani::proof]` to be applied to harnesses that use `spawn` as well. For this to happen, the user has to specify a scheduling strategy.
Co-authored-by: Celina G. Val <[email protected]>
It must be possible, when specifying methods, to refer to the type that the interface is implemented on. For example, an
add
method on ifacenum
, which takes an extra parameter of the same type and returns a value of the same type, can't be expressed in the current system without adding a lot of noisy type parameters.The
self
type is an implicit type parameter refers to the specialized type. An interface that uses it can not be cast to, since it'd be impossible to type its methods in the absence of a concrete self type.The text was updated successfully, but these errors were encountered: