fix: verso.code.warnLineLength warning

IrisTutorial/Basics.lean

@@ -198,7 +198,8 @@ is the Iris version of modus ponens. It is provable using only
 `iintro` and `iapply`.
 
 ```savedLean
-theorem modus_ponens (P Q : IProp GF) : P -∗ (P -∗ Q) -∗ Q := by
+theorem modus_ponens (P Q : IProp GF) :
+    P -∗ (P -∗ Q) -∗ Q := by
   iintro HP HPQ
   iapply HPQ
   iexact HP
@@ -313,7 +314,8 @@ Elimination of existentials uses the pattern `%x` (with a `%` in front
 of the bound variable) to move it to the pure (Lean) context.
 
 ```savedLean
-theorem sep_ex_distr {α : Type} (P : IProp GF) (Φ : α → IProp GF) :
+theorem sep_ex_distr {α : Type} (P : IProp GF)
+    (Φ : α → IProp GF) :
     (P ∗ ∃ x, Φ x) ⊣⊢ ∃ x, P ∗ Φ x := by
   isplit
   · iintro ⟨HP, %x, HΦ⟩

IrisTutorial/Lang.lean

@@ -70,14 +70,16 @@ def arith : Exp := hl(#1 + #2 * #3)
 The expected result of evaluating `arith` is `7`.
 
 ```savedLean
-def booleans : Exp := hl((#1 + #2 * #3 = #7) && #true || (#true = #false))
+def booleans : Exp :=
+  hl((#1 + #2 * #3 = #7) && #true || (#true = #false))
 ```
 
 The expected result is `#true`.
 
 ```savedLean
--- TODO (upstream — iris-lean): use the unit literal here once the
--- `hl` DSL gains a sugared form for `Val.lit BaseLit.unit`.
+-- TODO (upstream — iris-lean): use the unit
+-- literal here once the `hl` DSL gains a sugared form
+-- for `Val.lit BaseLit.unit`.
 def if_then_else : Exp := hl(if #true then #1 else #0)
 ```
 
@@ -150,7 +152,8 @@ def lambda : Exp :=
 
 ```savedLean
 def recursion : Exp :=
-  hl(let fac := (rec f n := if n = #0 then #1 else n * f (n - #1));
+  hl(let fac :=
+       (rec f n := if n = #0 then #1 else n * f (n - #1));
      (fac #4, fac #5))
 ```
 
@@ -209,8 +212,8 @@ compare-and-set, written `cas(l, v1, v2)`. The only difference is
 that `cas` only returns the boolean.
 
 ```savedLean
--- TODO (upstream — iris-lean): use the unit literal in the success
--- branches once the `hl` DSL gains a `#()` form.
+-- TODO (upstream — iris-lean): use the unit literal in the
+-- success branches once the `hl` DSL gains a `#()` form.
 def cas_example : Exp := hl(
   let l := ref(#5);
   if cas(l, #6, #7) then #0 else

IrisTutorial/LinkedLists.lean

@@ -53,7 +53,8 @@ values it represents.
 ```savedLean
 def isList (l : Val) : List Val → IProp GF
   | [] => iprop% ⌜l = hl_val(none())⌝
-  | x :: xs => iprop% ∃ hd l', ⌜l = hl_val(some(#(.loc hd)))⌝ ∗
+  | x :: xs => iprop% ∃ hd l',
+      ⌜l = hl_val(some(#(.loc hd)))⌝ ∗
       hd ↦ some hl_val((&x, &l')) ∗ isList l' xs
 ```
 
@@ -63,7 +64,8 @@ unfold and refold the predicate during proofs.
 
 ```savedLean
 theorem isList_nil {l} :
-    isList (GF := GF) l [] ⊣⊢ iprop(⌜l = hl_val(none())⌝) := .rfl
+    isList (GF := GF) l [] ⊣⊢
+      iprop(⌜l = hl_val(none())⌝) := .rfl
 ```
 
 ```savedLean
@@ -102,7 +104,8 @@ specification in postcondition-generic form — parametric in `Φ` and
 applied with `iapply`.
 
 ```savedLean
-theorem append_spec (l1 l2 : Val) (xs ys : List Val) (Φ : Val → IProp GF) :
+theorem append_spec (l1 l2 : Val) (xs ys : List Val)
+    (Φ : Val → IProp GF) :
     isList l1 xs -∗ isList l2 ys -∗
     (∀ v, isList v (xs ++ ys) -∗ Φ v) -∗
     WP hl(&append &l1 &l2) {{ Φ }} := by
@@ -179,7 +182,8 @@ induction. Unlike `append`, the accumulator `acc` and its list `ys`
 change on every recursive call, so we generalise over them too.
 
 ```savedLean
-theorem reverse_append_spec (l acc : Val) (xs ys : List Val) (Φ : Val → IProp GF) :
+theorem reverse_append_spec (l acc : Val)
+    (xs ys : List Val) (Φ : Val → IProp GF) :
     isList l xs -∗ isList acc ys -∗
     (∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗
     WP hl(&reverse_append &l &acc) {{ Φ }} := by
@@ -209,14 +213,17 @@ theorem reverse_append_spec (l acc : Val) (xs ys : List Val) (Φ : Val → IProp
     iintro !> Hpt
     wp_pures
     wp_bind (&reverse_append _ _)
-    ihave Hnode : isList hl_val(some(#(.loc hd))) (x :: ys) $$ [Hpt Hacc]
+    ihave Hnode :
+        isList hl_val(some(#(.loc hd))) (x :: ys) $$
+          [Hpt Hacc]
     · rw [isList]
       iexists hd, acc
       iframe
       itrivial
     iapply IH $$ Hl Hnode
     iintro %v Hv
-    simp only [List.reverse_cons, List.append_assoc, List.cons_append, List.nil_append]
+    simp only [List.reverse_cons, List.append_assoc,
+      List.cons_append, List.nil_append]
     iapply HΦ $$ Hv
 ```
 
@@ -225,7 +232,8 @@ accumulator represents the empty list, so `reverse l` returns the
 reverse of `l`.
 
 ```savedLean
-theorem reverse_spec (l : Val) (xs : List Val) (Φ : Val → IProp GF) :
+theorem reverse_spec (l : Val) (xs : List Val)
+    (Φ : Val → IProp GF) :
     isList l xs -∗
     (∀ v, isList v xs.reverse -∗ Φ v) -∗
     WP hl(&reverse &l) {{ Φ }} := by
@@ -279,13 +287,17 @@ it can be reused at every step of the induction.
 
 ```savedLean
 theorem fold_right_spec
-    (P : Val → IProp GF) (I : List Val → Val → IProp GF) (f a l : Val) (xs : List Val)
+    (P : Val → IProp GF)
+    (I : List Val → Val → IProp GF)
+    (f a l : Val) (xs : List Val)
     (Φ : Val → IProp GF) :
     isList l xs -∗
     ([∗list] _k ↦ x ∈ xs, P x) -∗
     I [] a -∗
     □ (∀ (x a' : Val) ys (Ψ : Val → IProp GF),
-        P x -∗ I ys a' -∗ (∀ r, I (x :: ys) r -∗ Ψ r) -∗ WP hl(&f &x &a') {{ Ψ }}) -∗
+        P x -∗ I ys a' -∗
+        (∀ r, I (x :: ys) r -∗ Ψ r) -∗
+        WP hl(&f &x &a') {{ Ψ }}) -∗
     (∀ r, isList l xs -∗ I xs r -∗ Φ r) -∗
     WP hl(&fold_right &f &a &l) {{ Φ }} := by
   iintro Hl HP HI #Hf HΦ

IrisTutorial/Persistently.lean

@@ -98,7 +98,8 @@ By contrast, putting `HP` into the spatial context discards
 persistency:
 
 ```savedLean
-theorem not_in_pers_context (P Q : IProp GF) [Persistent P] :
+theorem not_in_pers_context
+    (P Q : IProp GF) [Persistent P] :
     P -∗ Q -∗ P ∗ Q := by
   iintro HP HQ
   isplitr [HQ]
@@ -109,7 +110,8 @@ theorem not_in_pers_context (P Q : IProp GF) [Persistent P] :
 Persistent propositions are duplicable.
 
 ```savedLean
-theorem pers_dup (P : IProp GF) [Persistent P] : P ⊢ P ∗ P := by
+theorem pers_dup
+    (P : IProp GF) [Persistent P] : P ⊢ P ∗ P := by
   iintro #HP
   isplit
   · iexact HP
@@ -152,11 +154,13 @@ persistently modality is idempotent.
 theorem pers_idemp (P : IProp GF) : □ □ P ⊣⊢ □ P := by
   isplit
   · iintro #HP
-    -- Iris already knows that `□` is idempotent, so it
-    -- automatically removes all persistently modalities from a
-    -- proposition when adding it to the intuitionistic context.
-    -- One may think of all propositions in the intuitionistic
-    -- context as having an implicit `□` in front.
+    -- Iris already knows that `□` is idempotent, so
+    -- it automatically removes all persistently
+    -- modalities from a proposition when adding it
+    -- to the intuitionistic context.
+    -- One may think of all propositions in the
+    -- intuitionistic context as having an implicit
+    -- `□` in front.
     iexact HP
   · iintro #HP
     imodintro
@@ -169,7 +173,8 @@ for pure propositions, `Persistent` can automatically identify
 most persistent propositions.
 
 ```savedLean
-theorem pers_sep (P Q : IProp GF) : □ P ∗ □ Q ⊣⊢ □ (P ∗ Q) := by
+theorem pers_sep (P Q : IProp GF) :
+    □ P ∗ □ Q ⊣⊢ □ (P ∗ Q) := by
   isplit
   · iintro ⟨#HP, #HQ⟩
     imodintro
@@ -184,7 +189,8 @@ a persistent separation directly in the cases pattern.
 Persistency is preserved by quantifications.
 
 ```savedLean
-theorem pers_all {α : Type} (P : α → IProp GF) [∀ x, Persistent (P x)] :
+theorem pers_all {α : Type}
+    (P : α → IProp GF) [∀ x, Persistent (P x)] :
     (∀ x, □ P x) ⊢ ∀ y, P y ∗ P y := by
   iintro #Hp %y
   isplitl
@@ -196,7 +202,8 @@ For simple predicates such as the one below, Lean's typeclass
 resolution can automatically infer the `Persistent` instance.
 
 ```savedLean
-def myPredicate (x : Val) : IProp GF := iprop(⌜x = hl_val(#5)⌝)
+def myPredicate (x : Val) : IProp GF :=
+  iprop(⌜x = hl_val(#5)⌝)
 
 instance myPredicate_persistent (x : Val) :
     Persistent (myPredicate (GF := GF) x) := by
@@ -236,10 +243,12 @@ as persistent.
 theorem first_is_5 (x : Val) (xs : List Val) :
     myPredFix (GF := GF) (x :: xs) -∗
     ⌜x = hl_val(#5)⌝ ∗ myPredFix (x :: xs) := by
-  -- After `iintro #H`, the hypothesis `H : myPredFix (x :: xs)`
-  -- sits in the intuitionistic context. Since `myPredFix` unfolds
-  -- by pattern-matching, we can `change` the hypothesis-to-be so
-  -- the destructure exposes the head element.
+  -- After `iintro #H`, the hypothesis
+  -- `H : myPredFix (x :: xs)` sits in the
+  -- intuitionistic context. Since `myPredFix`
+  -- unfolds by pattern-matching, we can `change`
+  -- the hypothesis-to-be so the destructure
+  -- exposes the head element.
   show myPredFix (GF := GF) (x :: xs) -∗
        iprop(⌜x = hl_val(#5)⌝ ∗ myPredFix (x :: xs))
   change iprop(⌜x = hl_val(#5)⌝ ∗ myPredFix xs) -∗

IrisTutorial/Specifications.lean

@@ -92,7 +92,8 @@ def boolish : Exp := hl(
 ```
 
 ```savedLean
-theorem boolish_spec : ⊢@{IProp GF} WP boolish {{ v, ⌜v = hl_val(#1)⌝ }} := by
+theorem boolish_spec :
+    ⊢@{IProp GF} WP boolish {{ v, ⌜v = hl_val(#1)⌝ }} := by
   unfold boolish
   wp_pures
   itrivial
@@ -145,7 +146,8 @@ def hofun : Exp :=
 ```
 
 ```savedLean
-theorem hofun_spec : ⊢@{IProp GF} WP hofun {{ v, ⌜v = hl_val(#5)⌝ }} := by
+theorem hofun_spec :
+    ⊢@{IProp GF} WP hofun {{ v, ⌜v = hl_val(#5)⌝ }} := by
   unfold hofun
   wp_pures
   itrivial
@@ -215,7 +217,8 @@ def writeread : Exp := hl(
 
 ```savedLean
 theorem writeread_spec :
-    ⊢@{IProp GF} WP writeread {{ v, ⌜v = hl_val(#7)⌝ }} := by
+    ⊢@{IProp GF} WP writeread
+      {{ v, ⌜v = hl_val(#7)⌝ }} := by
   unfold writeread
   wp_bind ref(_)
   iapply wp_alloc
@@ -272,7 +275,8 @@ from the previous section.
 
 ```savedLean
 theorem writeread_spec_2 (Φ : Val → IProp GF) :
-    (∀ v, ⌜v = hl_val(#7)⌝ -∗ Φ v) -∗ WP writeread {{ v, Φ v }} := by
+    (∀ v, ⌜v = hl_val(#7)⌝ -∗ Φ v) -∗
+    WP writeread {{ v, Φ v }} := by
   iintro HΦ
   unfold writeread
   wp_bind ref(_)
@@ -389,7 +393,8 @@ def parWrite (l1 l2 : Loc) : Exp :=
 theorem parWrite_spec (l1 l2 : Loc) (v1 v2 : Val) :
     l1 ↦ some v1 -∗ l2 ↦ some v2 -∗
     WP (parWrite l1 l2)
-      {{ v, l1 ↦ some hl_val(#21) ∗ l2 ↦ some hl_val(#2) }} := by
+      {{ v, l1 ↦ some hl_val(#21) ∗
+            l2 ↦ some hl_val(#2) }} := by
   iintro Hl1 Hl2
   unfold parWrite
   iapply wp_par