dafny-lang · keyboardDrummer · Jan 12, 2024 · Jan 12, 2024 · Jan 12, 2024
diff --git a/docs/Compilation/AutoInitialization.md b/docs/Compilation/AutoInitialization.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Automatic Initialization of Variables
+---
 
 Automatic Initialization of Variables
 =====================================

diff --git a/docs/Compilation/Boogie.md b/docs/Compilation/Boogie.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Dafny compilation to Boogie
+---
 
 # Dafny compilation to Boogie
 

diff --git a/docs/Compilation/Go.md b/docs/Compilation/Go.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Dafny compilation to Go
+---
 
 Dafny compilation to Go
 =======================

diff --git a/docs/Compilation/ReferenceTypes.md b/docs/Compilation/ReferenceTypes.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Dafny compilation of trait and class
+---
 
 Dafny compilation of trait and class
 ====================================

diff --git a/docs/Compilation/StringsAndChars.md b/docs/Compilation/StringsAndChars.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Strings and Characters
+---
 
 # Strings and Characters
 

diff --git a/docs/HowToFAQ/FAQForallTricks.md b/docs/HowToFAQ/FAQForallTricks.md
@@ -1,10 +1,10 @@
 ---
-title: Why can't I write 'forall t: Test :: t.i == 1' for an object t?
+title: "Why can't I write `forall t: Test :: t.i == 1` for an object `t`?"
 ---
 
 ## Question:
 
-Why can't I write `forall t: Test :: t.i == 1` for an object t?
+Why can\'t I write `forall t: Test :: t.i == 1` for an object `t`?
 
 ## Answer:
 

diff --git a/docs/Installation.md b/docs/Installation.md
@@ -239,7 +239,7 @@ To setup Dafny to compile to python3:
 
 To separately compile and run your program for Python:
 - `dafny build -t:py MyProgram.dfy`
-- `python3 MyProgram-py/MyProgram.py
+- `python3 MyProgram-py/MyProgram.py`
 
 ### Rust
 

diff --git a/docs/OnlineTutorial/Lemmas.md b/docs/OnlineTutorial/Lemmas.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Lemmas and Induction
+---
 
 # Lemmas and Induction
 

diff --git a/docs/OnlineTutorial/Modules.md b/docs/OnlineTutorial/Modules.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Modules
+---
 
 # Modules
 

diff --git a/docs/OnlineTutorial/Sequences.md b/docs/OnlineTutorial/Sequences.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Sequences
+---
 
 # Sequences
 

diff --git a/docs/OnlineTutorial/Sets.md b/docs/OnlineTutorial/Sets.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Sets
+---
 
 # Sets
 

diff --git a/docs/OnlineTutorial/Termination.md b/docs/OnlineTutorial/Termination.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Termination
+---
 
 # Termination
 

diff --git a/docs/OnlineTutorial/ValueTypes.md b/docs/OnlineTutorial/ValueTypes.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Collection Types
+---
 
 # Collection Types
 

diff --git a/docs/OnlineTutorial/guide.md b/docs/OnlineTutorial/guide.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: "Getting Started with Dafny: A Guide"
+---
 
 # Getting Started with Dafny: A Guide
 

diff --git a/docs/QuickReference.md b/docs/QuickReference.md
@@ -1,5 +1,6 @@
-<p></p>
-<link rel="stylesheet" href="assets/main.css">
+---
+title: Dafny Quick Reference
+---
 
 # Dafny Quick Reference
 

diff --git a/docs/_config.yml b/docs/_config.yml
@@ -65,3 +65,11 @@ exclude:
  - vendor/cache/
  - vendor/gems/
  - vendor/ruby/
+ - "*.expect"
+
+defaults:
+ -
+ scope:
+ path: "" # an empty string here means all files in the project
+ values:
+ layout: "single"
diff --git a/docs/_layouts/single.html b/docs/_layouts/single.html
@@ -0,0 +1,18 @@
+<!DOCTYPE html>
+<html lang="{{ page.lang | default: site.lang | default: "en" }}">
+
+{%- include head.html -%}
+
+<body>
+
+ <main class="page-content" aria-label="Content">
+ <div class="wrapper">
+ {{ content }}
+ </div>
+ </main>
+
+ {%- include footer.html -%}
+
+</body>
+
+</html>