Deploying to gh-pages from @ eb5e8c2 🚀

induction_and_recursion.html

@@ -825,7 +825,7 @@ <h2><a class="header" href="#well-founded-recursion-and-induction" id="well-foun
   | 0,   y   =&gt; y+1
   | x+1, 0   =&gt; ack x 1
   | x+1, y+1 =&gt; ack x (ack (x+1) y)
-termination_by ack x y =&gt; (x, y)
+termination_by x y =&gt; (x, y)
 </code></pre>
 <p>Note that a lexicographic order is used in the example above because the instance
 <code>WellFoundedRelation (α × β)</code> uses a lexicographic order. Lean also defines the instance</p>
@@ -846,7 +846,7 @@ <h2><a class="header" href="#well-founded-recursion-and-induction" id="well-foun
         r
     else
       r
-termination_by go i r =&gt; as.size - i
+  termination_by as.size - i
 </code></pre>
 <p>Note that, auxiliary function <code>go</code> is recursive in this example, but <code>takeWhile</code> is not.</p>
 <p>By default, Lean uses the tactic <code>decreasing_tactic</code> to prove recursive applications are decreasing. The modifier <code>decreasing_by</code> allows us to provide our own tactic. Here is an example.</p>
@@ -865,11 +865,12 @@ <h2><a class="header" href="#well-founded-recursion-and-induction" id="well-foun
   | 0,   y   =&gt; y+1
   | x+1, 0   =&gt; ack x 1
   | x+1, y+1 =&gt; ack x (ack (x+1) y)
-termination_by ack x y =&gt; (x, y)
+termination_by x y =&gt; (x, y)
 decreasing_by
-  simp_wf -- unfolds well-founded recursion auxiliary definitions
-  first | apply Prod.Lex.right; simp_arith
-        | apply Prod.Lex.left; simp_arith
+  all_goals simp_wf -- unfolds well-founded recursion auxiliary definitions
+  · apply Prod.Lex.left; simp_arith
+  · apply Prod.Lex.right; simp_arith
+  · apply Prod.Lex.left; simp_arith
 </code></pre>
 <p>We can use <code>decreasing_by sorry</code> to instruct Lean to &quot;trust&quot; us that the function terminates.</p>
 <pre><code class="language-lean">def natToBin : Nat → List Nat

print.html

@@ -6796,7 +6796,7 @@ <h2><a class="header" href="#well-founded-recursion-and-induction" id="well-foun
   | 0,   y   =&gt; y+1
   | x+1, 0   =&gt; ack x 1
   | x+1, y+1 =&gt; ack x (ack (x+1) y)
-termination_by ack x y =&gt; (x, y)
+termination_by x y =&gt; (x, y)
 </code></pre>
 <p>Note that a lexicographic order is used in the example above because the instance
 <code>WellFoundedRelation (α × β)</code> uses a lexicographic order. Lean also defines the instance</p>
@@ -6817,7 +6817,7 @@ <h2><a class="header" href="#well-founded-recursion-and-induction" id="well-foun
         r
     else
       r
-termination_by go i r =&gt; as.size - i
+  termination_by as.size - i
 </code></pre>
 <p>Note that, auxiliary function <code>go</code> is recursive in this example, but <code>takeWhile</code> is not.</p>
 <p>By default, Lean uses the tactic <code>decreasing_tactic</code> to prove recursive applications are decreasing. The modifier <code>decreasing_by</code> allows us to provide our own tactic. Here is an example.</p>
@@ -6836,11 +6836,12 @@ <h2><a class="header" href="#well-founded-recursion-and-induction" id="well-foun
   | 0,   y   =&gt; y+1
   | x+1, 0   =&gt; ack x 1
   | x+1, y+1 =&gt; ack x (ack (x+1) y)
-termination_by ack x y =&gt; (x, y)
+termination_by x y =&gt; (x, y)
 decreasing_by
-  simp_wf -- unfolds well-founded recursion auxiliary definitions
-  first | apply Prod.Lex.right; simp_arith
-        | apply Prod.Lex.left; simp_arith
+  all_goals simp_wf -- unfolds well-founded recursion auxiliary definitions
+  · apply Prod.Lex.left; simp_arith
+  · apply Prod.Lex.right; simp_arith
+  · apply Prod.Lex.left; simp_arith
 </code></pre>
 <p>We can use <code>decreasing_by sorry</code> to instruct Lean to &quot;trust&quot; us that the function terminates.</p>
 <pre><code class="language-lean">def natToBin : Nat → List Nat