things are basically working!

Compile.hs

@@ -142,6 +142,8 @@ compileComment (Comment mayName comm) =
   <$> traverse compileBlock mayName <*> compileBlock comm
 
 compileTheoremStatement :: (Monad m, Applicative m) => TheoremStatement FullLocation -> Err m T.Text
+compileTheoremStatement (Prove b) =
+  (\bl -> div "theorem-statement" [tag' "h3" ["Prove"], bl]) <$> compileBlock b
 compileTheoremStatement (AssumeProve assumps results) =
   (\as rs ->
     div "theorem-statement" [

TranslateTex.hs

@@ -93,9 +93,11 @@ simpleSection keyword p = do
 labelAndStatement :: TexParser Ref (Maybe Label, TheoremStatement Ref)
 labelAndStatement = (,) <$> optLabel <*> (statement <* texSpace)
   where
-  statement =
+  statement = assumeProve <|> prove
+  assumeProve =
     AssumeProve <$> simpleSection "suppose" (many item)
                 <*> simpleSection "then" (many item)
+  prove = Prove <$> simpleSection "prove" (Block <$> many anyChunk)
 
 item = satisfy (== NoArgCmd "item") >> Block <$> many (satisfy (/= NoArgCmd "item"))
 

Types.hs

@@ -30,7 +30,11 @@ deriving instance Traversable (DeclarationF a)
 data Comment loc = Comment (Maybe (Tex.Block loc)) (Tex.Block loc)
   deriving (Show, Functor, Foldable, Traversable)
 
-data TheoremStatement loc = AssumeProve [Tex.Block loc] [Tex.Block loc]
+-- TODO: Clean this up. There needs to be a principled list of things
+-- here. Use types
+data TheoremStatement loc
+  = AssumeProve [Tex.Block loc] [Tex.Block loc]
+  | Prove (Tex.Block loc)
   deriving (Show, Functor, Foldable, Traversable)
 
 type MaybeJustifiedF a loc = (Tex.Block loc, Maybe (ProofF a loc))

examples/primes.tex

@@ -73,7 +73,7 @@
         \claim{Q.E.D.}
       }
       \claim{$a \leq \sqrt{n}$}{\simple{
-        $$a \leq \sqrt{m} \leq \sqrt{n}$$
+        $$a = \sqrt{\frac{m}{b}} \leq \sqrt{m} \leq \sqrt{n}$$
         which follows from the previous claim and monotonicity of $\sqrt{-}$.
       }}
       \claim{
@@ -98,16 +98,11 @@
   }
 
   \theorem{There are infinitely many prime numbers}{
-    \suppose{
-      \item There are finitely many primes.
-    }
-    \then{
-      \item Contradiction.
-    }
+    \prove{For any $N \in \bn$, there are at least $N$ primes}
 
     \proof{
       \suppose{\item $n \in \bn$}
-      \then{\item $\pi(n) \geq \frac{1}{2} \log n$}
+      \then{\item $\pi(n) \geq \frac{1}{2} \log_2 n$}
       \because{
         \claim{$2^{\pi(n)} \sqrt{n} \geq n$}{
           \claim{$2^{\pi(n)} \sqrt{n} \geq \rs{\mathcal{P}(\Pi(n)) \times \Set{1, \hdots, \floor{\sqrt{n}}}}$}{
@@ -141,11 +136,16 @@
         \claim{Q.E.D.}{\simple{Algebra.}}
       }
 
+      \claim{$\pi(2^{2 N}) \geq N$}{
+        \simple{
+          $$\pi(2^{2 N}) \geq \frac{1}{2} \log_2 2^{2N} = N$$
+        }
+      }
+
       \claim{Q.E.D.}{
         \simple{
-          Since the function $n \mapsto \frac{1}{2} \log n$ goes
-          to infinity with $n$, so too does $\pi(n)$.
-          By \ref{pidef}, this implies there are infinitely many primes.
+          The total number of primes is at least $\pi(2^{2 N})$,
+          so by the previous claim, there are at least $N$ primes.
         }
       }
     }

src/css/proof.css

@@ -103,19 +103,15 @@ body {
   font-family: 'Latin-Modern-Roman-Caps';
 }
 
-.take {
-  background-color: #e8dcc5;
-  padding: 10px;
-  margin: 10px;
-
-  border-radius: 23px 23px 23px 23px;
-  -moz-border-radius: 23px 23px 23px 23px;
-  -webkit-border-radius: 23px 23px 23px 23px;
-  border: 2px solid #000000;
+.list-header {
+  font-family: 'Latin-Modern-Roman-Caps';
 }
 
-.take .list-header {
-  font-family: 'Latin-Modern-Roman-Caps';
+.suppose {
+  border-left: 3px solid black;
+  padding-left: 10px;
+  margin-bottom: 5px;
+  margin-top: 5px;
 }
 
 .theorem {
@@ -126,10 +122,6 @@ body {
   display: inline-block;
 }
 
-.suchthat .list-header {
-  font-family: 'Latin-Modern-Roman-Caps';
-}
-
 .node-header {
   cursor: pointer;
 }

src/js/proof.js

@@ -82,7 +82,6 @@ function annotateWithNumbers(decls, level) {
 function decorateCaseBlocks(){
   $('.cases').each(function() {
     var block = $(this);
-    console.log('yo');
     block.prepend($('<div class="case-header">Cases:</div>'));
     // block.children('.case').each(function(i)
   });
@@ -132,6 +131,16 @@ function decorateSuchThats() {
   });
 }
 
+function decorateSupposes() {
+  $('.suppose').each(function() {
+    var suppose = $(this);
+    var assumptions = suppose.children('.assumptions');
+    var results     = suppose.children('.results');
+    assumptions.before($('<div class="list-header">Suppose:</div>'));
+    results.before($('<div class="list-header">Then:</div>'));
+  })
+}
+
 function wrapWithLocation(node) {
   var wrapper = $('<div class="wrapper">');
   node.replaceWith(wrapper);
@@ -169,6 +178,10 @@ function decorateComments() {
   });
 }
 
+function capitalize(s){
+  return s.charAt(0).toUpperCase() + s.substring(1);
+}
+
 function decorateTheorems() {
   $('.theorem').each(function() {
     var theorem   = $(this);
@@ -182,7 +195,8 @@ function decorateTheorems() {
     theorem.addClass('top-level');
 
     content.append(statement, proof);
-    header.append($('<h2>Theorem: </h2>'), name);
+    var title = capitalize(theorem.attr('data-thmkind'));
+    header.append($('<h2>' + title + ': </h2>'), name);
     theorem.append(header, content);
 
     var wrapper = $('<div class="wrapper">');
@@ -198,6 +212,7 @@ function decorateTheorems() {
 
 $(function(){
   MathJax.Hub.Queue(decorateCaseBlocks);
+  MathJax.Hub.Queue(decorateSupposes);
   MathJax.Hub.Queue(decorateTakes);
   MathJax.Hub.Queue(decorateLets);
   MathJax.Hub.Queue(decorateSuchThats);