diff --git a/nix/plutus-metatheory-site.nix b/nix/plutus-metatheory-site.nix
index 35f16431f26..e716eceb290 100644
--- a/nix/plutus-metatheory-site.nix
+++ b/nix/plutus-metatheory-site.nix
@@ -8,8 +8,12 @@ let
name = "plutus-metatheory-doc";
src = inputs.self + /plutus-metatheory;
buildInputs = [ repoRoot.nix.agda-with-stdlib ];
+
+ # Because of a quirk with jekyll, the _layouts folder must be in the same
+ # directory as the source folder.
buildPhase = ''
- mkdir "$out"
+ mkdir $out
+ cp -R ${inputs.self + /plutus-metatheory/html/_layouts} $out
agda --html --html-highlight=auto --html-dir="$out" "src/index.lagda.md"
'';
dontInstall = true;
@@ -21,7 +25,7 @@ let
}
''
mkdir "$out"
- # disable the disk cache otherwise it tries to write to the source
+ # Disable the disk cache otherwise it tries to write to the source
jekyll build \
--disable-disk-cache \
-s ${plutus-metatheory-agda-html} \
diff --git a/nix/shell.nix b/nix/shell.nix
index b4ee5c9d5bd..14ac3951c1b 100644
--- a/nix/shell.nix
+++ b/nix/shell.nix
@@ -46,6 +46,7 @@ in
pkgs.bzip2
pkgs.gawk
pkgs.scriv
+ pkgs.fswatch
# Needed to make building things work, not for commands
pkgs.zlib
@@ -79,6 +80,7 @@ in
group = "changelog";
};
+
shellHook = ''
${builtins.readFile certEnv}
'';
diff --git a/plutus-metatheory/.gitignore b/plutus-metatheory/.gitignore
index 6df8d5dcde3..36d1ebf59e0 100644
--- a/plutus-metatheory/.gitignore
+++ b/plutus-metatheory/.gitignore
@@ -2,3 +2,8 @@
*.lagda~
*.agda~
src/MAlonzo
+html/_site
+html/.jekyll-cache
+html/*.html
+html/*.md
+html/*.css
diff --git a/plutus-metatheory/README.md b/plutus-metatheory/README.md
index 3a52985fad6..441925d2b54 100644
--- a/plutus-metatheory/README.md
+++ b/plutus-metatheory/README.md
@@ -80,8 +80,8 @@ $ cabal test plutus-metatheory
To build the documentation as a static site:
```
-$ agda --html --html-highlight=auto --html-dir html src/index.lagda.md
-$ jekyll -s html -d site
+$ agda --html --html-highlight=auto --html-dir=html src/index.lagda.md
+$ jekyll build -s html -d html/_site
```
## Features:
diff --git a/plutus-metatheory/html/_layouts/page.html b/plutus-metatheory/html/_layouts/page.html
new file mode 100644
index 00000000000..34c608149dd
--- /dev/null
+++ b/plutus-metatheory/html/_layouts/page.html
@@ -0,0 +1,14 @@
+
+
+
+
+ {{ page.title }}
+
+
+
+ {{ page.title }}
+
+
+
\ No newline at end of file
diff --git a/plutus-metatheory/src/Algorithmic.lagda.md b/plutus-metatheory/src/Algorithmic.lagda.md
index c2b7d68764a..f4a71a6dd4f 100644
--- a/plutus-metatheory/src/Algorithmic.lagda.md
+++ b/plutus-metatheory/src/Algorithmic.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic
+layout: page
+---
```
module Algorithmic where
```
@@ -335,4 +339,4 @@ constr-cong' : ∀{Γ : Ctx Φ}{n}{i : Fin n}{A : Vec (List (Φ ⊢Nf⋆ *)) n}
→ (q : subst (IList (Γ ⊢_)) p' cs' ≡ subst (IList (Γ ⊢_)) p cs)
→ constr i A p' cs' ≡ constr i A p cs
constr-cong' refl refl refl = refl
-```
\ No newline at end of file
+```
diff --git a/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CCvsCK.lagda.md b/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CCvsCK.lagda.md
index 1695a7f0041..7d4ab0e1ba8 100644
--- a/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CCvsCK.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CCvsCK.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.BehaviouralEquivalence.CCvsCK
+layout: page
+---
# CK machine
```
diff --git a/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CKvsCEK.lagda.md b/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CKvsCEK.lagda.md
index ed4bd820b86..7a40b7f9f10 100644
--- a/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CKvsCEK.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CKvsCEK.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.BehaviouralEquivalence.CCvsCEK
+layout: page
+---
# CEK behavioural equivalence with CK machine
```
diff --git a/plutus-metatheory/src/Algorithmic/CEK.lagda.md b/plutus-metatheory/src/Algorithmic/CEK.lagda.md
index 3ab56f1c241..321dae4a290 100644
--- a/plutus-metatheory/src/Algorithmic/CEK.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/CEK.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.CEK
+layout: page
+---
# CEK machine that discharges builtin args
```
diff --git a/plutus-metatheory/src/Algorithmic/CK.lagda.md b/plutus-metatheory/src/Algorithmic/CK.lagda.md
index bf32c1c0710..83b627d7f77 100644
--- a/plutus-metatheory/src/Algorithmic/CK.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/CK.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.CK
+layout: page
+---
# CK machine
```
diff --git a/plutus-metatheory/src/Algorithmic/Completeness.lagda.md b/plutus-metatheory/src/Algorithmic/Completeness.lagda.md
index deda4d82d20..fd0fa2affc2 100644
--- a/plutus-metatheory/src/Algorithmic/Completeness.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Completeness.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Completeness
+layout: page
+---
```
module Algorithmic.Completeness where
diff --git a/plutus-metatheory/src/Algorithmic/Erasure.lagda.md b/plutus-metatheory/src/Algorithmic/Erasure.lagda.md
index c2638ef463d..9b658d1530a 100644
--- a/plutus-metatheory/src/Algorithmic/Erasure.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Erasure.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Erasure
+layout: page
+---
```
{-# OPTIONS --injective-type-constructors #-}
diff --git a/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda.md b/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda.md
index 7eca7b9424c..c27e8d0dcbc 100644
--- a/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Erasure.RenamingSubstitution
+layout: page
+---
```
module Algorithmic.Erasure.RenamingSubstitution where
```
diff --git a/plutus-metatheory/src/Algorithmic/Evaluation.lagda.md b/plutus-metatheory/src/Algorithmic/Evaluation.lagda.md
index 410c7ab315b..2d4c5b558d3 100644
--- a/plutus-metatheory/src/Algorithmic/Evaluation.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Evaluation.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Evaluation
+layout: page
+---
```
module Algorithmic.Evaluation where
```
@@ -85,4 +89,4 @@ stepper {A} t n with eval (gas n) t
... | steps x (error _) = return (error A)
```
-
\ No newline at end of file
+
diff --git a/plutus-metatheory/src/Algorithmic/Examples.lagda.md b/plutus-metatheory/src/Algorithmic/Examples.lagda.md
index 08ccda7a4e8..113d5120720 100644
--- a/plutus-metatheory/src/Algorithmic/Examples.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Examples.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Examples
+layout: page
+---
```
module Algorithmic.Examples where
```
diff --git a/plutus-metatheory/src/Algorithmic/Properties.lagda.md b/plutus-metatheory/src/Algorithmic/Properties.lagda.md
index 055df253906..97b390b2f80 100644
--- a/plutus-metatheory/src/Algorithmic/Properties.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Properties.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Properties
+layout: page
+---
```
module Algorithmic.Properties where
```
diff --git a/plutus-metatheory/src/Algorithmic/Reduction.lagda.md b/plutus-metatheory/src/Algorithmic/Reduction.lagda.md
index b07e1b9fbfc..2fed602dcca 100644
--- a/plutus-metatheory/src/Algorithmic/Reduction.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Reduction.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Reduction
+layout: page
+---
```
module Algorithmic.Reduction where
```
diff --git a/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md b/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md
index 8f95dcaaab7..6a90b8e297f 100644
--- a/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.ReductionEC
+layout: page
+---
```
module Algorithmic.ReductionEC where
```
@@ -371,4 +375,4 @@ ival : ∀ b → Value (builtin b / refl)
ival b = V-I b base
-- -}
```
-
\ No newline at end of file
+
diff --git a/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md b/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md
index feaef184d64..301f6b14217 100644
--- a/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.ReductionEC.Determinism
+layout: page
+---
```
module Algorithmic.ReductionEC.Determinism where
```
@@ -684,4 +688,4 @@ determinism {L = L} (ruleErr E' p) (ruleErr E'' q) | step ¬VL E err r' U with U
... | refl ,, refl ,, refl | refl ,, refl ,, refl = refl
-- -}
```
-
\ No newline at end of file
+
diff --git a/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md b/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md
index e726bb099a0..dd25415ce47 100644
--- a/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.ReductionEC.Progress
+layout: page
+---
```
module Algorithmic.ReductionEC.Progress where
```
@@ -139,4 +143,4 @@ progress (case M cases) with progress M
... | step (ruleErr E refl) = step (ruleErr (case cases E) refl)
... | done (V-constr e Tss refl refl vs refl) = step (ruleEC [] (β-case e Tss refl vs refl cases) refl refl)
-
\ No newline at end of file
+
diff --git a/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda.md b/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda.md
index a37eea391a1..02e1e9cd2b9 100644
--- a/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.RenamingSubstitution
+layout: page
+---
```
module Algorithmic.RenamingSubstitution where
```
@@ -591,4 +595,4 @@ exts⋆ˢ : ∀{Φ}{Γ Δ : Ctx Φ}
-}
```
-
\ No newline at end of file
+
diff --git a/plutus-metatheory/src/Algorithmic/Signature.lagda.md b/plutus-metatheory/src/Algorithmic/Signature.lagda.md
index 88eea3fbbc6..ad9cf4b9722 100644
--- a/plutus-metatheory/src/Algorithmic/Signature.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Signature.lagda.md
@@ -1,4 +1,7 @@
-
+---
+title: Algorithmic.Signature
+layout: page
+---
```
module Algorithmic.Signature where
```
@@ -94,4 +97,4 @@ uniqueSigTy (bresult _) (bresult _) = refl
uniqueSigTy (A B⇒ s) (.A B⇒ s') = cong (A B⇒_) (uniqueSigTy s s')
uniqueSigTy (sucΠ s) (sucΠ s') = cong sucΠ (uniqueSigTy s s')
```
-
\ No newline at end of file
+
diff --git a/plutus-metatheory/src/Algorithmic/Soundness.lagda.md b/plutus-metatheory/src/Algorithmic/Soundness.lagda.md
index 418e9d41778..46c8188e0ba 100644
--- a/plutus-metatheory/src/Algorithmic/Soundness.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Soundness.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Soundness
+layout: page
+---
```
module Algorithmic.Soundness where
diff --git a/plutus-metatheory/src/Builtin.lagda.md b/plutus-metatheory/src/Builtin.lagda.md
index 7d34f632a19..f216d83f945 100644
--- a/plutus-metatheory/src/Builtin.lagda.md
+++ b/plutus-metatheory/src/Builtin.lagda.md
@@ -184,22 +184,22 @@ hence need to be embedded into `n⋆ / n♯ ⊢⋆` using the postfix constructo
list : ∀{n⋆ n♯} → n♯ ⊢♯ → n⋆ / n♯ ⊢⋆
list a = (blist a) ↑
- ```
+```
- ###Operators for constructing signatures
-
- The following operators are used to express signatures in a familiar way,
- but ultimately, they construct a Sig
+### Operators for constructing signatures
- An expression
- n⋆×n♯ [ t₁ , t₂ , t₃ ]⟶ tᵣ
-
- is actually parsed as
- (((n⋆×n♯ [ t₁) , t₂) , t₃) ]⟶ tᵣ
-
- and constructs a signature
+The following operators are used to express signatures in a familiar way,
+but ultimately, they construct a Sig
+
+An expression
+ n⋆×n♯ [ t₁ , t₂ , t₃ ]⟶ tᵣ
+
+is actually parsed as
+ (((n⋆×n♯ [ t₁) , t₂) , t₃) ]⟶ tᵣ
+
+and constructs a signature
- sig n⋆ n♯ (t₃ ∷ t₂ ∷ t₁) tᵣ
+sig n⋆ n♯ (t₃ ∷ t₂ ∷ t₁) tᵣ
```
ArgSet : Set
diff --git a/plutus-metatheory/src/Builtin/Constant/AtomicType.lagda.md b/plutus-metatheory/src/Builtin/Constant/AtomicType.lagda.md
index 39e0405604a..8e79bd8d526 100644
--- a/plutus-metatheory/src/Builtin/Constant/AtomicType.lagda.md
+++ b/plutus-metatheory/src/Builtin/Constant/AtomicType.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Builtin.Constant.AtomicType
+layout: page
+---
```
module Builtin.Constant.AtomicType where
diff --git a/plutus-metatheory/src/Check.lagda.md b/plutus-metatheory/src/Check.lagda.md
index dce238100f4..eaad6869c60 100644
--- a/plutus-metatheory/src/Check.lagda.md
+++ b/plutus-metatheory/src/Check.lagda.md
@@ -1,4 +1,5 @@
---
+title: Type Checker
layout: page
---
## Type checker
diff --git a/plutus-metatheory/src/Cost.lagda.md b/plutus-metatheory/src/Cost.lagda.md
index 9ecbcc525e7..6f0ceaa50be 100644
--- a/plutus-metatheory/src/Cost.lagda.md
+++ b/plutus-metatheory/src/Cost.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Cost
+layout: page
+---
# Costs
diff --git a/plutus-metatheory/src/Cost/Base.lagda.md b/plutus-metatheory/src/Cost/Base.lagda.md
index 184f3d9b465..66a57678041 100644
--- a/plutus-metatheory/src/Cost/Base.lagda.md
+++ b/plutus-metatheory/src/Cost/Base.lagda.md
@@ -1,4 +1,7 @@
-
+---
+title: Cost.Base
+layout: page
+---
```
module Cost.Base where
@@ -92,4 +95,4 @@ record MachineParameters (Cost : Set) : Set where
startupCost : Cost
startupCost = cekMachineCost BStartup
-```
\ No newline at end of file
+```
diff --git a/plutus-metatheory/src/Cost/Model.lagda.md b/plutus-metatheory/src/Cost/Model.lagda.md
index 74cf58ce95e..4af0668ea3d 100644
--- a/plutus-metatheory/src/Cost/Model.lagda.md
+++ b/plutus-metatheory/src/Cost/Model.lagda.md
@@ -1,4 +1,7 @@
-
+---
+title: Cost.Model
+layout: page
+---
# Builtin Cost Models
```
diff --git a/plutus-metatheory/src/Cost/Raw.lagda.md b/plutus-metatheory/src/Cost/Raw.lagda.md
index b01d5ea183f..8c2074a957e 100644
--- a/plutus-metatheory/src/Cost/Raw.lagda.md
+++ b/plutus-metatheory/src/Cost/Raw.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Cost.Raw
+layout: page
+---
# Raw Cost structures to inferface with Haskell
```
diff --git a/plutus-metatheory/src/Cost/Size.lagda.md b/plutus-metatheory/src/Cost/Size.lagda.md
index 0e1e33e9ce2..86776e130de 100644
--- a/plutus-metatheory/src/Cost/Size.lagda.md
+++ b/plutus-metatheory/src/Cost/Size.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Cost.Size
+layout: page
+---
# Size of Constants
```
@@ -83,4 +87,4 @@ defaultConstantMeasure (tmCon (pair t u) (x , y)) =
defaultValueMeasure : Value → CostingNat
defaultValueMeasure (V-con ty x) = defaultConstantMeasure (tmCon ty x)
defaultValueMeasure _ = 0
-```
\ No newline at end of file
+```
diff --git a/plutus-metatheory/src/Declarative/Examples/StdLib/ChurchNat.lagda.md b/plutus-metatheory/src/Declarative/Examples/StdLib/ChurchNat.lagda.md
index 7cc7104870a..e565fd65a0d 100644
--- a/plutus-metatheory/src/Declarative/Examples/StdLib/ChurchNat.lagda.md
+++ b/plutus-metatheory/src/Declarative/Examples/StdLib/ChurchNat.lagda.md
@@ -1,3 +1,7 @@
+---
+title: ChurchNat
+layout: page
+---
```
module Declarative.Examples.StdLib.ChurchNat where
```
diff --git a/plutus-metatheory/src/Declarative/Examples/StdLib/Function.lagda.md b/plutus-metatheory/src/Declarative/Examples/StdLib/Function.lagda.md
index 83ab8ef832f..5b90ee636d0 100644
--- a/plutus-metatheory/src/Declarative/Examples/StdLib/Function.lagda.md
+++ b/plutus-metatheory/src/Declarative/Examples/StdLib/Function.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Function
+layout: page
+---
```
module Declarative.Examples.StdLib.Function where
```
diff --git a/plutus-metatheory/src/Declarative/Examples/StdLib/Nat.lagda.md b/plutus-metatheory/src/Declarative/Examples/StdLib/Nat.lagda.md
index f27ad6cf27e..09e30eb0977 100644
--- a/plutus-metatheory/src/Declarative/Examples/StdLib/Nat.lagda.md
+++ b/plutus-metatheory/src/Declarative/Examples/StdLib/Nat.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Nat
+layout: page
+---
```
module Declarative.Examples.StdLib.Nat where
```
diff --git a/plutus-metatheory/src/Evaluator/Base.lagda.md b/plutus-metatheory/src/Evaluator/Base.lagda.md
index ab12c3e9e54..522661916ec 100644
--- a/plutus-metatheory/src/Evaluator/Base.lagda.md
+++ b/plutus-metatheory/src/Evaluator/Base.lagda.md
@@ -1,4 +1,7 @@
-
+---
+title: Base
+layout: page
+---
```
module Evaluator.Base where
@@ -104,4 +107,4 @@ reportError (runtimeError runtimeTypeError) = "runtimeTypeError"
```
maxsteps : Nat
maxsteps = 10000000000
-```
\ No newline at end of file
+```
diff --git a/plutus-metatheory/src/Evaluator/Program.lagda.md b/plutus-metatheory/src/Evaluator/Program.lagda.md
index f289e8beba9..2c6d8c5b28f 100644
--- a/plutus-metatheory/src/Evaluator/Program.lagda.md
+++ b/plutus-metatheory/src/Evaluator/Program.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Program Evaluators
+layout: page
+---
# Evaluators for Programs
```
@@ -227,4 +231,4 @@ typeCheckProgramN namedprog = do
-}
return (prettyPrintTy (unshifterTy Z (extricateScopeTy (extricateNf⋆ A))))
```
-
\ No newline at end of file
+
diff --git a/plutus-metatheory/src/Evaluator/Term.lagda.md b/plutus-metatheory/src/Evaluator/Term.lagda.md
index 254f15d906d..526705ed553 100644
--- a/plutus-metatheory/src/Evaluator/Term.lagda.md
+++ b/plutus-metatheory/src/Evaluator/Term.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Term - Haskell Interface to the Metatheory
+layout: page
+---
# Haskell Interface to the metatheory
This module contains functions that are meant to be called from Haskell code.
@@ -336,4 +340,4 @@ alphaU plc1 plc2 | inj₂ plc1' | inj₂ plc2' | _ | _ = Bool.false
alphaU plc1 plc2 | _ | _ = Bool.false
{-# COMPILE GHC alphaU as alphaU #-}
-```
\ No newline at end of file
+```
diff --git a/plutus-metatheory/src/Main.lagda.md b/plutus-metatheory/src/Main.lagda.md
index 92350cceb1b..3f50c43491a 100644
--- a/plutus-metatheory/src/Main.lagda.md
+++ b/plutus-metatheory/src/Main.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Main
+layout: page
+---
```
module Main where
diff --git a/plutus-metatheory/src/Raw.lagda.md b/plutus-metatheory/src/Raw.lagda.md
index 743ad028ea0..556999458e1 100644
--- a/plutus-metatheory/src/Raw.lagda.md
+++ b/plutus-metatheory/src/Raw.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Raw
+layout: page
+---
```
module Raw where
```
@@ -180,4 +184,4 @@ rawListPrinter [] = ""
rawListPrinter (x ∷ []) = rawPrinter x
rawListPrinter (x ∷ y ∷ xs) = rawPrinter x ++ " , " ++ rawListPrinter (y ∷ xs)
```
-
\ No newline at end of file
+
diff --git a/plutus-metatheory/src/RawU.lagda.md b/plutus-metatheory/src/RawU.lagda.md
index 706457c26b9..b5f0af9fa98 100644
--- a/plutus-metatheory/src/RawU.lagda.md
+++ b/plutus-metatheory/src/RawU.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Raw - Interface to Haskell
+layout: page
+---
This module provides the interface between the Haskell code and the Agda code.
It replicates the Haskell representation of Raw. In particular, for term constants,
diff --git a/plutus-metatheory/src/Scoped.lagda.md b/plutus-metatheory/src/Scoped.lagda.md
index 4ea4bf0bb4f..6a8c80c13b7 100644
--- a/plutus-metatheory/src/Scoped.lagda.md
+++ b/plutus-metatheory/src/Scoped.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Scoped
+layout: page
+---
```
module Scoped where
```
diff --git a/plutus-metatheory/src/Scoped/Extrication.lagda.md b/plutus-metatheory/src/Scoped/Extrication.lagda.md
index 0250e0963a7..04395a8eb77 100644
--- a/plutus-metatheory/src/Scoped/Extrication.lagda.md
+++ b/plutus-metatheory/src/Scoped/Extrication.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Scoped.Extrication
+layout: page
+---
```
module Scoped.Extrication where
```
diff --git a/plutus-metatheory/src/Scoped/Extrication/RenamingSubstitution.lagda.md b/plutus-metatheory/src/Scoped/Extrication/RenamingSubstitution.lagda.md
index 5731dabe73b..67497acaa9a 100644
--- a/plutus-metatheory/src/Scoped/Extrication/RenamingSubstitution.lagda.md
+++ b/plutus-metatheory/src/Scoped/Extrication/RenamingSubstitution.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Scoped.Extrication.RenamingSubstitution
+layout: page
+---
```
module Scoped.Extrication.RenamingSubstitution where
```
diff --git a/plutus-metatheory/src/Scoped/RenamingSubstitution.lagda.md b/plutus-metatheory/src/Scoped/RenamingSubstitution.lagda.md
index 141afe7e917..8ec242565d6 100644
--- a/plutus-metatheory/src/Scoped/RenamingSubstitution.lagda.md
+++ b/plutus-metatheory/src/Scoped/RenamingSubstitution.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Scoped.RenamingSubstitution
+layout: page
+---
```
module Scoped.RenamingSubstitution where
```
diff --git a/plutus-metatheory/src/Type/BetaNBE.lagda.md b/plutus-metatheory/src/Type/BetaNBE.lagda.md
index 8e896de1d2f..75288d17d32 100644
--- a/plutus-metatheory/src/Type/BetaNBE.lagda.md
+++ b/plutus-metatheory/src/Type/BetaNBE.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Type.BetaNBE
+layout: page
+---
```
module Type.BetaNBE where
```
@@ -187,4 +191,4 @@ module _ where
→ lookup (eval-VecList Tss η) e ≡ eval-List (lookup Tss e) η
lookup-eval-VecList zero (_ ∷ _) η = refl
lookup-eval-VecList (suc e) (_ ∷ Tss) η = lookup-eval-VecList e Tss η
-```
\ No newline at end of file
+```
diff --git a/plutus-metatheory/src/Type/BetaNBE/Completeness.lagda.md b/plutus-metatheory/src/Type/BetaNBE/Completeness.lagda.md
index f289c166b74..d740d8102f6 100644
--- a/plutus-metatheory/src/Type/BetaNBE/Completeness.lagda.md
+++ b/plutus-metatheory/src/Type/BetaNBE/Completeness.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Type.BetaNBE.Completeness
+layout: page
+---
```
module Type.BetaNBE.Completeness where
```
diff --git a/plutus-metatheory/src/Type/BetaNBE/RenamingSubstitution.lagda.md b/plutus-metatheory/src/Type/BetaNBE/RenamingSubstitution.lagda.md
index 8771f68d1b5..4dd3863bcc2 100644
--- a/plutus-metatheory/src/Type/BetaNBE/RenamingSubstitution.lagda.md
+++ b/plutus-metatheory/src/Type/BetaNBE/RenamingSubstitution.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Type.BetaNBE.RenamingSubstitution
+layout: page
+---
```
module Type.BetaNBE.RenamingSubstitution where
diff --git a/plutus-metatheory/src/Type/BetaNBE/Soundness.lagda.md b/plutus-metatheory/src/Type/BetaNBE/Soundness.lagda.md
index d03c9feafdd..dc5c6e364e2 100644
--- a/plutus-metatheory/src/Type/BetaNBE/Soundness.lagda.md
+++ b/plutus-metatheory/src/Type/BetaNBE/Soundness.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Type.BetaNBE.Soundness
+layout: page
+---
```
module Type.BetaNBE.Soundness where
```
diff --git a/plutus-metatheory/src/Type/BetaNBE/Stability.lagda.md b/plutus-metatheory/src/Type/BetaNBE/Stability.lagda.md
index 327490aa7b6..f07bc23d42b 100644
--- a/plutus-metatheory/src/Type/BetaNBE/Stability.lagda.md
+++ b/plutus-metatheory/src/Type/BetaNBE/Stability.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Type.BetaNBE.Stability
+layout: page
+---
```
module Type.BetaNBE.Stability where
```
diff --git a/plutus-metatheory/src/Type/BetaNormal.lagda.md b/plutus-metatheory/src/Type/BetaNormal.lagda.md
index 6e64fb85bdf..bcbc7771fd4 100644
--- a/plutus-metatheory/src/Type/BetaNormal.lagda.md
+++ b/plutus-metatheory/src/Type/BetaNormal.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Type.BetaNormal
+layout: page
+---
```
module Type.BetaNormal where
```
diff --git a/plutus-metatheory/src/Type/BetaNormal/Equality.lagda.md b/plutus-metatheory/src/Type/BetaNormal/Equality.lagda.md
index 2adcfa29454..4ffcd817ee2 100644
--- a/plutus-metatheory/src/Type/BetaNormal/Equality.lagda.md
+++ b/plutus-metatheory/src/Type/BetaNormal/Equality.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Type.BetaNormal.Equality
+layout: page
+---
```
module Type.BetaNormal.Equality where
```
@@ -134,4 +138,4 @@ renNf-comp-VecList [] = refl
renNf-comp-VecList (xs ∷ xss) = cong₂ _∷_ (renNf-comp-List xs) (renNf-comp-VecList xss)
```
-
\ No newline at end of file
+
diff --git a/plutus-metatheory/src/Untyped/CEK.lagda.md b/plutus-metatheory/src/Untyped/CEK.lagda.md
index 6a0ebfe4c79..f3915779ca4 100644
--- a/plutus-metatheory/src/Untyped/CEK.lagda.md
+++ b/plutus-metatheory/src/Untyped/CEK.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Untyped.CEK
+layout: page
+---
```
{-# OPTIONS --type-in-type #-}
diff --git a/plutus-metatheory/src/Untyped/CEKWithCost.lagda.md b/plutus-metatheory/src/Untyped/CEKWithCost.lagda.md
index dff944ff137..635fba0b62d 100644
--- a/plutus-metatheory/src/Untyped/CEKWithCost.lagda.md
+++ b/plutus-metatheory/src/Untyped/CEKWithCost.lagda.md
@@ -1,3 +1,7 @@
+---
+title: CEK Machine with Costs
+layout: page
+---
# CEK Machine with costs
This module implements a CEK machine for UPLC which computes costs.
@@ -227,4 +231,4 @@ cekStepperEquivalence (suc n) s rewrite sym (cekStepEquivalence s) with step s
... | s ◅ v = cekStepperEquivalence n (s ◅ v)
... | □ x = refl
... | ◆ = refl
-```
\ No newline at end of file
+```
diff --git a/plutus-metatheory/src/Utils.lagda.md b/plutus-metatheory/src/Utils.lagda.md
index cbeba0e86ce..94216fbff09 100644
--- a/plutus-metatheory/src/Utils.lagda.md
+++ b/plutus-metatheory/src/Utils.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Utils
+layout: page
+---
```
module Utils where
```
diff --git a/plutus-metatheory/src/Utils/Decidable.lagda.md b/plutus-metatheory/src/Utils/Decidable.lagda.md
index 5723eafaa32..3da35c2920a 100644
--- a/plutus-metatheory/src/Utils/Decidable.lagda.md
+++ b/plutus-metatheory/src/Utils/Decidable.lagda.md
@@ -1,4 +1,7 @@
-
+---
+title: Utils.Decidable
+layout: page
+---
```
module Utils.Decidable where
```
@@ -54,4 +57,4 @@ dhcong₂ : ∀ {α β γ} {A : Set α} {B B' : A → Set β} {C : Set γ} {x₁
→ Dec (f x₁ y₁ z₁ ≡ f x₂ y₂ z₂)
dhcong₂ f inj (yes refl) qy qz = dcong₂ (f _) ((λ { (refl ,, yy) → yy }) ∘ inj) (qy _) (qz _)
dhcong₂ f inj (no c) _ _ = no λ {p → c (proj₁ (inj p))}
-```
\ No newline at end of file
+```
diff --git a/plutus-metatheory/src/Utils/List.lagda.md b/plutus-metatheory/src/Utils/List.lagda.md
index bee5c93b3a3..e4ea65f6bc0 100644
--- a/plutus-metatheory/src/Utils/List.lagda.md
+++ b/plutus-metatheory/src/Utils/List.lagda.md
@@ -1,4 +1,7 @@
-
+---
+title: Utils.List
+layout: page
+---
```
module Utils.List where
```
@@ -509,4 +512,4 @@ equalbyPredicateI {bs = bs}{bs'}{fs}{fs'}{tot} TOT {Bs} {Bs'} {Fs} {Fs'} {h} {h'
... | pbs , snd with <>>[]-cancelʳ bs bs' pbs
equalbyPredicateI TOT {Bs} {Bs'} P p p' q q' ps ps' ¬PH ¬PH'
| refl , refl , refl , pBs | refl with <>>I[]-cancelʳ Bs Bs' pBs
-... | refl = refl , refl , refl , refl
\ No newline at end of file
+... | refl = refl , refl , refl , refl
diff --git a/plutus-metatheory/src/Utils/Reflection.lagda.md b/plutus-metatheory/src/Utils/Reflection.lagda.md
index 8406a97a6be..7547d6b78bf 100644
--- a/plutus-metatheory/src/Utils/Reflection.lagda.md
+++ b/plutus-metatheory/src/Utils/Reflection.lagda.md
@@ -1,4 +1,7 @@
-
+---
+title: Utils.Reflection
+layout: page
+---
```
module Utils.Reflection where
@@ -118,4 +121,4 @@ defListConstructors T defName = do
d ← getDefinition T
let cls = clause [] [] (mkList (map (λ q → con q []) (constructors d)))
defineFun defName (cls ∷ [])
-```
\ No newline at end of file
+```