pub struct FnOutput {
pub returns: FnRetTy,
pub ensures: Vec<Ensures>,
pub node_id: NodeId,
}
Fields§
§returns: FnRetTy
example i32{v:v >= 0}
ensures: Vec<Ensures>
example: *x: i32{v. v = n+1}
or just x > 10
node_id: NodeId
Trait Implementations§
Auto Trait Implementations§
impl Freeze for FnOutput
impl RefUnwindSafe for FnOutput
impl Send for FnOutput
impl Sync for FnOutput
impl Unpin for FnOutput
impl UnwindSafe for FnOutput
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more