Update mer. 17 juil. 2024 18:05:05 CEST

leanprover-community · Jul 17, 2024 · 35b2b0c · 35b2b0c
1 parent 27a1a3f
commit 35b2b0c
Show file tree

Hide file tree

Showing 30 changed files with 1,340 additions and 14,126 deletions.
diff --git a/.buildinfo b/.buildinfo
@@ -1,4 +1,4 @@
 # Sphinx build info version 1
 # This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
-config: 803b947a09f3db5a52c6c529e3761a53
+config: dfa3c760a9c309561b2de03685612f6b
 tags: 645f666f9bcd5a90fca523b33c5a78b7
diff --git a/C01_Introduction.html b/C01_Introduction.html
@@ -1,7 +1,8 @@
 <!DOCTYPE html>
 <html class="writer-html5" lang="en" >
 <head>
-  <meta charset="utf-8" />
+  <meta charset="utf-8" /><meta name="generator" content="Docutils 0.18.1: http://docutils.sourceforge.net/" />
+
   <meta name="viewport" content="width=device-width, initial-scale=1.0" />
   <title>1. Introduction &mdash; Mathematics in Lean 0.1 documentation</title>
       <link rel="stylesheet" href="_static/pygments.css" type="text/css" />
@@ -12,10 +13,11 @@
     <script src="_static/js/html5shiv.min.js"></script>
   <![endif]-->
 
-        <script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
         <script src="_static/jquery.js"></script>
-        <script src="_static/underscore.js"></script>
+        <script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
+        <script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
         <script src="_static/doctools.js"></script>
+        <script src="_static/sphinx_highlight.js"></script>
     <script src="_static/js/theme.js"></script>
     <link rel="index" title="Index" href="genindex.html" />
     <link rel="search" title="Search" href="search.html" />
@@ -28,11 +30,15 @@
     <nav data-toggle="wy-nav-shift" class="wy-nav-side">
       <div class="wy-side-scroll">
         <div class="wy-side-nav-search" >
-            <a href="index.html" class="icon icon-home"> Mathematics in Lean
+
+
+
+          <a href="index.html" class="icon icon-home">
+            Mathematics in Lean
           </a>
 <div role="search">
   <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
-    <input type="text" name="q" placeholder="Search docs" />
+    <input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
     <input type="hidden" name="check_keywords" value="yes" />
     <input type="hidden" name="area" value="default" />
   </form>
@@ -72,8 +78,8 @@
         <div class="rst-content">
           <div role="navigation" aria-label="Page navigation">
   <ul class="wy-breadcrumbs">
-      <li><a href="index.html" class="icon icon-home"></a> &raquo;</li>
-      <li><span class="section-number">1. </span>Introduction</li>
+      <li><a href="index.html" class="icon icon-home" aria-label="Home"></a></li>
+      <li class="breadcrumb-item active"><span class="section-number">1. </span>Introduction</li>
       <li class="wy-breadcrumbs-aside">
             <a href="_sources/C01_Introduction.rst.txt" rel="nofollow"> View page source</a>
       </li>
@@ -83,10 +89,10 @@
           <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
            <div itemprop="articleBody">
 
-  <div class="section" id="introduction">
-<span id="id1"></span><h1><span class="section-number">1. </span>Introduction<a class="headerlink" href="#introduction" title="Permalink to this headline">&#61633;</a></h1>
-<div class="section" id="getting-started">
-<h2><span class="section-number">1.1. </span>Getting Started<a class="headerlink" href="#getting-started" title="Permalink to this headline">&#61633;</a></h2>
+  <section id="introduction">
+<span id="id1"></span><h1><span class="section-number">1. </span>Introduction<a class="headerlink" href="#introduction" title="Permalink to this heading">&#61633;</a></h1>
+<section id="getting-started">
+<h2><span class="section-number">1.1. </span>Getting Started<a class="headerlink" href="#getting-started" title="Permalink to this heading">&#61633;</a></h2>
 <p>The goal of this book is to teach you to formalize mathematics using the
 Lean 4 interactive proof assistant.
 It assumes that you know some mathematics, but it does not require much.
@@ -171,9 +177,9 @@ <h2><span class="section-number">1.1. </span>Getting Started<a class="headerlink
 the relevant skills, feel free to move on.
 You can always compare your solutions to the ones in the <code class="docutils literal notranslate"><span class="pre">solutions</span></code>
 folder associated with each section.</p>
-</div>
-<div class="section" id="overview">
-<h2><span class="section-number">1.2. </span>Overview<a class="headerlink" href="#overview" title="Permalink to this headline">&#61633;</a></h2>
+</section>
+<section id="overview">
+<h2><span class="section-number">1.2. </span>Overview<a class="headerlink" href="#overview" title="Permalink to this heading">&#61633;</a></h2>
 <p>Put simply, Lean is a tool for building complex expressions in a formal language
 known as <em>dependent type theory</em>.</p>
 <p id="index-0">Every expression has a <em>type</em>, and you can use the <cite>#check</cite> command to
@@ -347,8 +353,8 @@ <h2><span class="section-number">1.2. </span>Overview<a class="headerlink" href=
 Floris van Doorn, and Eric Wieser.
 Our work has been partially supported by the Hoskinson Center for
 Formal Mathematics.</p>
-</div>
-</div>
+</section>
+</section>
 
 
            </div>