moving confluence to src/plfa

extra/extra/Confluence.lagda

@@ -1,13 +1,21 @@
+---
+title     : "Substitution in the untyped lambda calculus"
+layout    : page
+prev      : /Substitution/
+permalink : /Confluence/
+next      : /Denotational/
+---
+
 \begin{code}
-module extra.Confluence where
+module plfa.Confluence where
 \end{code}
 
 ## Imports
 
 \begin{code}
-open import extra.Substitution
+open import plfa.Substitution
     using (subst-commute; rename-subst-commute)
-open import extra.LambdaReduction
+open import plfa.LambdaReduction
     using (_—→_; β; ξ₁; ξ₂; ζ; _—↠_; _—→⟨_⟩_; _[];
            abs-cong; appL-cong; appR-cong;
            —↠-trans)

src/plfa/Adequacy.lagda

@@ -3,7 +3,7 @@ title     : "Adequacy: of denotational semantics with respect to operational sem
 layout    : page
 prev      : /Soundness/
 permalink : /Adequacy/
-next      : /Acknowledgements/
+next      : /CallByName/
 ---
 
 \begin{code}

src/plfa/CallByName.lagda

@@ -1,3 +1,11 @@
+---
+title     : "Call by name reduction of the untyped lambda calculus"
+layout    : page
+prev      : /Adequacy/
+permalink : /CallByName/
+next      : /Acknowledgements/
+---
+
 \begin{code}
 module plfa.CallByName where
 \end{code}

src/plfa/Soundness.lagda

@@ -16,7 +16,7 @@ module plfa.Soundness where
 open import plfa.Untyped
   using (Context; _,_; _∋_; _⊢_; ★; Z; S_; `_; ƛ_; _·_;
          subst; _[_]; subst-zero; ext; rename; exts)
-open import extra.LambdaReduction
+open import plfa.LambdaReduction
   using (_—→_; ξ₁; ξ₂; β; ζ; _—↠_; _—→⟨_⟩_; _[])
 open import plfa.Denotational
 open import plfa.Compositional

src/plfa/Substitution.lagda

@@ -1,3 +1,12 @@
+---
+title     : "Substitution in the untyped lambda calculus"
+layout    : page
+prev      : /Untyped/
+permalink : /Substitution/
+next      : /Confluence/
+---
+
+
 \begin{code}
 module plfa.Substitution where
 \end{code}