Skip to content

Commit

Permalink
add missing "supertrait" bounds
Browse files Browse the repository at this point in the history
  • Loading branch information
juliand665 committed Feb 15, 2023
1 parent d23dbd5 commit 077c0e0
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion prusti-contracts/prusti-contracts/src/core_spec/option.rs
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ impl<T> Option<T> {
F: FnOnce() -> T;

#[ensures(old(self.is_none()) || old(self) === Some(result))]
#[refine_spec(where T: super::default::PureDefault, [
#[refine_spec(where T: Copy + super::default::PureDefault, [
ensures(result === match old(self) {
Some(v) => v,
None => Default::default(),
Expand Down
2 changes: 1 addition & 1 deletion prusti-contracts/prusti-contracts/src/core_spec/result.rs
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ impl<T, E> Result<T, E> {
E: Debug;

#[ensures(old(self.is_err()) || old(self) === Ok(result))]
#[refine_spec(where T: super::default::PureDefault, [
#[refine_spec(where T: Copy + super::default::PureDefault, [
ensures(result === match old(self) {
Ok(v) => v,
Err(_) => T::default(),
Expand Down

0 comments on commit 077c0e0

Please sign in to comment.