Enable pdf export

.readthedocs.yaml

@@ -15,8 +15,8 @@ sphinx:
    configuration: docs/source/conf.py
 
 # Optionally build your docs in additional formats such as PDF
-formats: []
-   # - pdf
+formats:
+   - pdf
 
 # Optionally declare the Python requirements required to build your docs
 python:

docs/source/compiler/core/core-language.md

@@ -131,11 +131,11 @@ $$
 
 Sorts $∗_i$ are explicitly levelled. Dependent function types, dependent conjunction types, and type annotations include a usage annotation $π$.
 
-Judgements have the following form:
+<!-- Judgements have the following form:
 
 $$ x_1 \overset{ρ_1}{:} S_1, ..., x_n \overset{ρ_n}{:} S_n \vdash\ M \overset{σ}{:} T $$
 
-where $ρ_1 ... ρ_n$ are elements of the semiring and $σ$ is either the $0$ or $1$ of the semiring.
+where $ρ_1 ... ρ_n$ are elements of the semiring and $σ$ is either the $0$ or $1$ of the semiring. -->
 
 Further define the syntactic categories of usages $ρ, π$ and precontexts $Γ$:
 

docs/source/compiler/core/index.md

@@ -6,7 +6,6 @@ maxdepth: 1
 ---
 
 core-language
-elementary-affine-core
 erased-core-language
 termination-checking
 ```

docs/source/compiler/frontend/index.md

@@ -8,6 +8,7 @@ maxdepth: 1
 ---
 
 features/index
+syntax-guide
 s-expression-syntax
 desugar
 ```

docs/source/getting-started/tutorials/syntax-guide.md → docs/source/compiler/frontend/syntax-guide.md

@@ -6,12 +6,12 @@ This page is subject to change with the syntax redesign.
 ```
 
 ## Syntax Guide
-This document is heavily inspired by the [[http://docs.idris-lang.org/en/latest/reference/syntax-guide.html][Idris syntax guide]].
+This document is heavily inspired by the [Idris syntax guide](http://docs.idris-lang.org/en/latest/reference/syntax-guide.html).
 
 ## File Organization
-A file contains zero or more [[Top Level Declarations]]
+A file contains zero or more [top level declarations](#top-level-declarations). 
 
-For example
+For example:
 ```haskell
   -- this is a function with a signature!
   sig foo : Natural
@@ -340,7 +340,7 @@ Example:
       True
     | else = False
 ```
-##### Dependent matching
+#### Dependent matching
 
 ### Definitions
 Definitions within an expression are like their top level