Deploying to gh-pages from @ leanprover/theorem_proving_in_lean4@81b0283

 🚀

dependent_type_theory.html

@@ -877,7 +877,8 @@ <h2><a class="header" href="#what-makes-dependent-type-theory-dependent" id="wha
 the Cartesian product <code>α × β</code> in the same way. Dependent products
 are also called <em>sigma</em> types, and you can also write them as
 <code>Σ a : α, β a</code>. You can use <code>⟨a, b⟩</code> or <code>Sigma.mk a b</code> to create a
-dependent pair.</p>
+dependent pair.  The <code>⟨</code> and <code>⟩</code> characters may be typed with
+<code>\langle</code> and <code>\rangle</code> or <code>\&lt;</code> and <code>\&gt;</code>, respectively.</p>
 <pre><code class="language-lean">universe u v
 
 def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=

print.html

@@ -966,7 +966,8 @@ <h2><a class="header" href="#what-makes-dependent-type-theory-dependent" id="wha
 the Cartesian product <code>α × β</code> in the same way. Dependent products
 are also called <em>sigma</em> types, and you can also write them as
 <code>Σ a : α, β a</code>. You can use <code>⟨a, b⟩</code> or <code>Sigma.mk a b</code> to create a
-dependent pair.</p>
+dependent pair.  The <code>⟨</code> and <code>⟩</code> characters may be typed with
+<code>\langle</code> and <code>\rangle</code> or <code>\&lt;</code> and <code>\&gt;</code>, respectively.</p>
 <pre><code class="language-lean">universe u v
 
 def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=