From e1145086676af4e9415ae3bf5f591475f57dc60e Mon Sep 17 00:00:00 2001
From: mimo31 <viktor.fukala@gmail.com>
Date: Sat, 15 Jul 2023 20:29:06 +0200
Subject: [PATCH] Add missing ignore to snippets in the user guide

---
 docs/user-guide/src/verify/resources_obligations.md | 3 +--
 docs/user-guide/src/verify/time_reasoning.md        | 6 +++---
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/docs/user-guide/src/verify/resources_obligations.md b/docs/user-guide/src/verify/resources_obligations.md
index e0f0367e248..ed465c1b572 100644
--- a/docs/user-guide/src/verify/resources_obligations.md
+++ b/docs/user-guide/src/verify/resources_obligations.md
@@ -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).
 
@@ -27,7 +27,6 @@ resource! {
 The general syntax is
 
 ```rust,noplaypen,ignore
-
 resource! {
     fn resource_name(amount: usize, ...);
 }
diff --git a/docs/user-guide/src/verify/time_reasoning.md b/docs/user-guide/src/verify/time_reasoning.md
index f7c41d575c8..fa15036b57a 100644
--- a/docs/user-guide/src/verify/time_reasoning.md
+++ b/docs/user-guide/src/verify/time_reasoning.md
@@ -22,7 +22,7 @@ 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) {
@@ -30,14 +30,14 @@ 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) {