Skip to content

Commit

Permalink
Add missing ignore to snippets in the user guide
Browse files Browse the repository at this point in the history
  • Loading branch information
vfukala committed Jul 15, 2023
1 parent 600a4b0 commit e114508
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 5 deletions.
3 changes: 1 addition & 2 deletions docs/user-guide/src/verify/resources_obligations.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# Resources and Obligations
# Resources and obligations

One way of describing state that is otherwise not captured by a Prusti program is using resources and obligations. They are typically produced and consumed by [`#[trusted]`](trusted.md) functions that have some external effects (e.g. by calling functions in foreign non-Rust libraries or by interacting with the real world).

Expand Down Expand Up @@ -27,7 +27,6 @@ resource! {
The general syntax is

```rust,noplaypen,ignore
resource! {
fn resource_name(amount: usize, ...);
}
Expand Down
6 changes: 3 additions & 3 deletions docs/user-guide/src/verify/time_reasoning.md
Original file line number Diff line number Diff line change
Expand Up @@ -22,22 +22,22 @@ The number of time steps a function needs to execute might also depend on the in

The following are three more equivalent ways of specifying the same precondition of `do_work` as above.

```rust,noplaygen
```rust,noplaygen,ignore
#[requires(time_credits(6))]
#[requires(if more_work { time_credits(5) } else { true })]
fn do_work(more_work: bool) {
// ...
}
```

```rust,noplaypen
```rust,noplaypen,ignore
#[requires(time_credits(6) & (more_work ==> time_credits(5)))]
fn do_work(more_work: bool) {
// ...
}
```

```rust,noplaypen
```rust,noplaypen,ignore
#[requires(more_work ==> time_credits(11))]
#[requires(!more_work ==> time_credits(6))]
fn do_work(more_work: bool) {
Expand Down

0 comments on commit e114508

Please sign in to comment.