Deploying to gh-pages from @ 048b6bb 🚀

leanprover · Mar 1, 2024 · 7b3f114 · 7b3f114
1 parent 7116efa
commit 7b3f114
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 6 deletions.
diff --git a/dependent_type_theory.html b/dependent_type_theory.html
@@ -400,8 +400,8 @@ <h2><a class="header" href="#function-abstraction-and-evaluation" id="function-a
 from an expression as follows:</p>
 <pre><code class="language-lean">#check fun (x : Nat) =&gt; x + 5   -- Nat → Nat
 #check λ (x : Nat) =&gt; x + 5     -- λ and fun mean the same thing
-#check fun x : Nat =&gt; x + 5     -- Nat inferred
-#check λ x : Nat =&gt; x + 5       -- Nat inferred
+#check fun x =&gt; x + 5     -- Nat inferred
+#check λ x =&gt; x + 5       -- Nat inferred
 </code></pre>
 <p>You can evaluate a lambda function by passing the required parameters:</p>
 <pre><code class="language-lean">#eval (λ x : Nat =&gt; x + 5) 10    -- 15

diff --git a/print.html b/print.html
@@ -489,8 +489,8 @@ <h2><a class="header" href="#function-abstraction-and-evaluation" id="function-a
 from an expression as follows:</p>
 <pre><code class="language-lean">#check fun (x : Nat) =&gt; x + 5   -- Nat → Nat
 #check λ (x : Nat) =&gt; x + 5     -- λ and fun mean the same thing
-#check fun x : Nat =&gt; x + 5     -- Nat inferred
-#check λ x : Nat =&gt; x + 5       -- Nat inferred
+#check fun x =&gt; x + 5     -- Nat inferred
+#check λ x =&gt; x + 5       -- Nat inferred
 </code></pre>
 <p>You can evaluate a lambda function by passing the required parameters:</p>
 <pre><code class="language-lean">#eval (λ x : Nat =&gt; x + 5) 10    -- 15

diff --git a/searchindex.js b/searchindex.js
diff --git a/searchindex.json b/searchindex.json