Update Sat Nov 11 16:52:07 EST 2023

hrmacbeth · Nov 11, 2023 · 30e9d92 · 30e9d92
1 parent a46e8ec
commit 30e9d92
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 9 deletions.
diff --git a/Homework.html b/Homework.html
@@ -554,7 +554,7 @@
 <span class="math notranslate nohighlight">\(x\)</span>, with <span class="math notranslate nohighlight">\(x\)</span> odd, such that <span class="math notranslate nohighlight">\(n=2^ax\)</span>.</p>
 <p>Suggested approach: strong induction; start with a case split on the parity of <span class="math notranslate nohighlight">\(n\)</span>,
 using the lemma <code class="docutils literal notranslate"><span class="pre">Nat.even_or_odd</span></code>.</p>
-<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="c">/-</span><span class="cm"> 5 points -/</span>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[autograded 5]</span>
 <span class="kd">theorem</span> <span class="n">problem1</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">a</span> <span class="n">x</span><span class="o">,</span> <span class="n">Odd</span> <span class="n">x</span> <span class="bp">&#8743;</span> <span class="n">n</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">^</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">x</span> <span class="o">:=</span> <span class="kd">by</span>
   <span class="gr">sorry</span>
 </pre></div>
@@ -564,7 +564,7 @@
 for all natural numbers <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span>, <span class="math notranslate nohighlight">\(P_{a,b} =P_{b,a}\)</span>.</p>
 <p>Suggested approach: well-founded induction, following the Lean template provided below.
 (I have filled in everything except for the main inductive step.)</p>
-<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="c">/-</span><span class="cm"> 5 points -/</span>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[autograded 5]</span>
 <span class="kd">theorem</span> <span class="n">problem2</span> <span class="o">(</span><span class="n">m</span> <span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="o">:</span> <span class="n">pascal</span> <span class="n">m</span> <span class="n">n</span> <span class="bp">=</span> <span class="n">pascal</span> <span class="n">n</span> <span class="n">m</span> <span class="o">:=</span> <span class="kd">by</span>
   <span class="k">match</span> <span class="n">m</span><span class="o">,</span> <span class="n">n</span> <span class="k">with</span>
   <span class="bp">|</span> <span class="mi">0</span><span class="o">,</span> <span class="mi">0</span> <span class="bp">=&gt;</span> <span class="n">rw</span> <span class="o">[</span><span class="n">pascal</span><span class="o">]</span>
@@ -589,11 +589,11 @@
 <span class="math notranslate nohighlight">\(\mathbb{R}\)</span> is surjective.</p>
 <p>(If you think it&#8217;s true, prove it, by solving the first version below.  If you think it&#8217;s false,
 solve the second version.)</p>
-<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="c">/-</span><span class="cm"> 4 points -/</span>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[autograded 4]</span>
 <span class="kd">theorem</span> <span class="n">problem4a</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
   <span class="gr">sorry</span>
 
-<span class="c">/-</span><span class="cm"> 4 points -/</span>
+<span class="kd">@[autograded 4]</span>
 <span class="kd">theorem</span> <span class="n">problem4b</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
   <span class="gr">sorry</span>
 </pre></div>
@@ -603,11 +603,11 @@
 <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span> is surjective.</p>
 <p>(If you think it&#8217;s true, prove it, by solving the first version below.  If you think it&#8217;s false,
 solve the second version.)</p>
-<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="c">/-</span><span class="cm"> 5 points -/</span>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[autograded 5]</span>
 <span class="kd">theorem</span> <span class="n">problem5a</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
   <span class="gr">sorry</span>
 
-<span class="c">/-</span><span class="cm"> 5 points -/</span>
+<span class="kd">@[autograded 5]</span>
 <span class="kd">theorem</span> <span class="n">problem5b</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
   <span class="gr">sorry</span>
 </pre></div>
@@ -618,11 +618,11 @@
 <span class="math notranslate nohighlight">\(\mathbb{Q}\)</span> is also injective.</p>
 <p>(If you think it&#8217;s true, prove it, by solving the first version below.  If you think it&#8217;s false,
 solve the second version.)</p>
-<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="c">/-</span><span class="cm"> 5 points -/</span>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[autograded 5]</span>
 <span class="kd">theorem</span> <span class="n">problem6a</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">&#8594;</span> <span class="n">&#8474;</span><span class="o">),</span> <span class="n">Injective</span> <span class="n">f</span> <span class="bp">&#8594;</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="n">x</span> <span class="bp">&#8614;</span> <span class="n">f</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
   <span class="gr">sorry</span>
 
-<span class="c">/-</span><span class="cm"> 5 points -/</span>
+<span class="kd">@[autograded 5]</span>
 <span class="kd">theorem</span> <span class="n">problem6b</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">&#8594;</span> <span class="n">&#8474;</span><span class="o">),</span> <span class="n">Injective</span> <span class="n">f</span> <span class="bp">&#8594;</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="n">x</span> <span class="bp">&#8614;</span> <span class="n">f</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
   <span class="gr">sorry</span>
 </pre></div>