diff --git a/website/docs/heyvl/README.md b/website/docs/heyvl/README.md
index 8bf6a1d..77b3166 100644
--- a/website/docs/heyvl/README.md
+++ b/website/docs/heyvl/README.md
@@ -9,24 +9,10 @@ The main innovation is that it supports _quantitative_ reasoning via its constru
 Refer to our [publications](../publications.md) for details on the theory.
 
 A HeyVL file consists of a sequence of declarations: [procedure](./procs.md) and [domain declarations](./domains.md).
+Refer to those for more information.
 
 ```mdx-code-block
 import DocCardList from '@theme/DocCardList';
 
 <DocCardList />
 ```
-
-## Use the source, Luke
-
-We do not formally describe the syntax of HeyVL in this documentation.
-You can find a more formal definition in the [`src/front/parser/grammar.lalrpop`](https://github.com/moves-rwth/caesar/blob/main/src/front/parser/grammar.lalrpop) file that specifies the syntax used to generate Caesar's parser.
-It is written in the [LALRPOP language](https://lalrpop.github.io/lalrpop/tutorial/index.html).
-
-## Examples
-
-The [`pgcl/examples-heyvl`](https://github.com/moves-rwth/caesar/tree/main/pgcl/examples-heyvl) directory contains the machine-translated HeyVL code for our pGCL examples.
-Note that they are just sequences of HeyVL statements without wrapping procedure declarations.
-Refer to the page on the [pGCL frontend](../pgcl.md) for more information.
-
-Caesar's integration tests in [`tests/`](https://github.com/moves-rwth/caesar/tree/main/tests) can also serve as a reference.
-Refer to the [development guide](../devguide.md#caesar) for more information about these tests.
diff --git a/website/docs/heyvl/procs.md b/website/docs/heyvl/procs.md
index 9dbb250..78e2d7f 100644
--- a/website/docs/heyvl/procs.md
+++ b/website/docs/heyvl/procs.md
@@ -48,7 +48,9 @@ Let us decompose the example into its parts:
  3. We have one **output parameter** `x` of type [`UInt`](../stdlib/numbers.md#uint).
     - There may be multiple parameters (input and output), which can be separated by commas (e.g. `init_x: UInt, init_y: UInt`).
  4. The `pre` declares the **pre-expectation** `init_x + 0.5`. It is evaluated in the *initial state* (when calling the proc). This is why it is called "pre" (= before running the proc).
+    - The `pre` is an expression of type [`EUReal`](../stdlib/numbers.md#eureal) over the input parameters.
  5. The `post` is the **post-expectation** `x` and evaluated in the final states of the proc (post = after running the proc). We always compare its expected value against the pre.
+    - The `post` is an expression of type [`EUReal`](../stdlib/numbers.md#eureal) over the input and output parameters.
  6. The **body of the proc** assigns `init_x` to `x`. We then do a [probabilistic coin flip](../stdlib/distributions.md#symbolic-with-probabilities) and assign `true` to `prob_choice` with probability `0.5` (and `false` with probability `0.5`). It determines the expected value ($\mathbb{E}$) we look at.
     - See [documentation on statements](./statements.md) for more information.
     - [The body is optional](#procs-without-body).
diff --git a/website/docusaurus.config.js b/website/docusaurus.config.js
index 56182d7..1a387c4 100644
--- a/website/docusaurus.config.js
+++ b/website/docusaurus.config.js
@@ -173,6 +173,11 @@ const config = {
         darkTheme: prismThemes.nightOwl,
         additionalLanguages: ['bash', 'shell-session'],
       },
+      algolia: {
+        appId: 'Q93W1TPDIE',
+        apiKey: '8dc15a6ca0d7a01e9f7ab673468d63a1',
+        indexName: 'caesarverifier',
+      }
     }),
 };
 
diff --git a/website/src/css/custom.css b/website/src/css/custom.css
index 9bba272..3870d3f 100644
--- a/website/src/css/custom.css
+++ b/website/src/css/custom.css
@@ -41,15 +41,15 @@
 }
 
 /* Link decorations */
-p a, .markdown ul a {
+.markdown p a, .markdown ul a {
   --ifm-link-decoration: underline;
 }
 
-p a:hover, .markdown ul a:hover {
+.markdown p a:hover, .markdown ul a:hover {
   text-decoration: none;
 }
 
-a.button {
+.markdown a.button {
   text-decoration: none;
 }