Added markdown titles to markdown files so they get built properly. N…

…ot all of the titles are very interesting.

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
-```
+```

plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CCvsCK.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Algorithmic.BehaviouralEquivalence.CCvsCK
+layout: page
+---
 # CK machine
 
 ```

plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CKvsCEK.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Algorithmic.BehaviouralEquivalence.CCvsCEK
+layout: page
+---
 # CEK behavioural equivalence with CK machine
 
 ```

plutus-metatheory/src/Algorithmic/CEK.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Algorithmic.CEK
+layout: page
+---
 # CEK machine that discharges builtin args
 
 ```

plutus-metatheory/src/Algorithmic/CK.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Algorithmic.CK
+layout: page
+---
 # CK machine
 
 ```

plutus-metatheory/src/Algorithmic/Completeness.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Completeness
+layout: page
+---
 ```
 module Algorithmic.Completeness where
 

plutus-metatheory/src/Algorithmic/Erasure.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Erasure
+layout: page
+---
 ```
 {-# OPTIONS --injective-type-constructors #-}
 

plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Erasure.RenamingSubstitution
+layout: page
+---
 ```
 module Algorithmic.Erasure.RenamingSubstitution where
 ```

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)
 
 ```
-
+

plutus-metatheory/src/Algorithmic/Examples.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Examples
+layout: page
+---
 ```
 module Algorithmic.Examples where
 ```

plutus-metatheory/src/Algorithmic/Properties.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Properties
+layout: page
+---
 ```
 module Algorithmic.Properties where
 ```

plutus-metatheory/src/Algorithmic/Reduction.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Reduction
+layout: page
+---
 ```
 module Algorithmic.Reduction where
 ```

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
 -- -}
 ```
-
+

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
 -- -}
 ```  
-
+

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)
 
- 
+ 

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 Φ}
 -}
 ```
 
-
+

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') 
 ```
-
+

plutus-metatheory/src/Algorithmic/Soundness.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Soundness
+layout: page
+---
 ```
 module Algorithmic.Soundness where
 

plutus-metatheory/src/Builtin/Constant/AtomicType.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Builtin.Constant.AtomicType
+layout: page
+---
 
 ```
 module Builtin.Constant.AtomicType where

plutus-metatheory/src/Check.lagda.md

@@ -1,4 +1,5 @@
 ---
+title: Type Checker
 layout: page
 ---
 ## Type checker

plutus-metatheory/src/Cost.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Cost
+layout: page
+---
 # Costs
 
 

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
-``` 
+``` 

plutus-metatheory/src/Cost/Model.lagda.md

@@ -1,4 +1,7 @@
-
+---
+title: Cost.Model
+layout: page
+---
 # Builtin Cost Models
 
 ```

plutus-metatheory/src/Cost/Raw.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Cost.Raw
+layout: page
+---
 # Raw Cost structures to inferface with Haskell
 
 ```

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
-```
+```

plutus-metatheory/src/Declarative/Examples/StdLib/ChurchNat.lagda.md

@@ -1,3 +1,7 @@
+---
+title: ChurchNat
+layout: page
+---
 ```
 module Declarative.Examples.StdLib.ChurchNat where
 ```

plutus-metatheory/src/Declarative/Examples/StdLib/Function.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Function
+layout: page
+---
 ```
 module Declarative.Examples.StdLib.Function where
 ```

plutus-metatheory/src/Declarative/Examples/StdLib/Nat.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Nat
+layout: page
+---
 ```
 module Declarative.Examples.StdLib.Nat where
 ```

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
-```
+```

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))))
 ```
-
+

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 #-}
-```
+```

plutus-metatheory/src/Main.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Main
+layout: page
+---
 ```
 module Main where
 

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)                               
 ```
-
+

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,

plutus-metatheory/src/Scoped.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Scoped
+layout: page
+---
 ```
 module Scoped where
 ```

plutus-metatheory/src/Scoped/Extrication.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Scoped.Extrication
+layout: page
+---
 ```
 module Scoped.Extrication where
 ```

plutus-metatheory/src/Scoped/Extrication/RenamingSubstitution.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Scoped.Extrication.RenamingSubstitution
+layout: page
+---
 ```
 module Scoped.Extrication.RenamingSubstitution where
 ```

plutus-metatheory/src/Scoped/RenamingSubstitution.lagda.md

@@ -1,3 +1,7 @@
+---
+title: Scoped.RenamingSubstitution
+layout: page
+---
 ```
 module Scoped.RenamingSubstitution where
 ```