From cf7a3e630c883dd69a8e71e880fe52cae825df9c Mon Sep 17 00:00:00 2001 From: wadler Date: Wed, 4 Jul 2018 18:40:17 -0300 Subject: [PATCH] moving plta to plfa --- Notes.md | 5 ++++ _config.yml | 5 ++-- src/{ => plfa}/plta/Acknowledgements.lagda | 0 src/{ => plfa}/plta/Bisimulation.lagda | 0 src/{ => plfa}/plta/Connectives.lagda | 2 +- src/{ => plfa}/plta/DeBruijn.lagda | 2 +- src/{ => plfa}/plta/Decidable.lagda | 2 +- src/{ => plfa}/plta/Equality.lagda | 2 +- src/{ => plfa}/plta/Fonts.lagda | 30 +++++++++++++++++----- src/{ => plfa}/plta/Induction.lagda | 2 +- src/{ => plfa}/plta/Inference.lagda | 2 +- src/{ => plfa}/plta/Isomorphism.lagda | 2 +- src/{ => plfa}/plta/Lambda.lagda | 2 +- src/{ => plfa}/plta/Lists.lagda | 2 +- src/{ => plfa}/plta/Modules.lagda | 2 +- src/{ => plfa}/plta/More.lagda | 2 +- src/{ => plfa}/plta/Naturals.lagda | 2 +- src/{ => plfa}/plta/Negation.lagda | 2 +- src/{ => plfa}/plta/Preface.lagda | 4 --- src/{ => plfa}/plta/Properties.lagda | 2 +- src/{ => plfa}/plta/Quantifiers.lagda | 2 +- src/{ => plfa}/plta/Relations.lagda | 2 +- src/{ => plfa}/plta/Statistics.lagda | 4 --- src/{ => plfa}/plta/Untyped.lagda | 2 +- 24 files changed, 47 insertions(+), 35 deletions(-) rename src/{ => plfa}/plta/Acknowledgements.lagda (100%) rename src/{ => plfa}/plta/Bisimulation.lagda (100%) rename src/{ => plfa}/plta/Connectives.lagda (99%) rename src/{ => plfa}/plta/DeBruijn.lagda (99%) rename src/{ => plfa}/plta/Decidable.lagda (99%) rename src/{ => plfa}/plta/Equality.lagda (99%) rename src/{ => plfa}/plta/Fonts.lagda (69%) rename src/{ => plfa}/plta/Induction.lagda (99%) rename src/{ => plfa}/plta/Inference.lagda (99%) rename src/{ => plfa}/plta/Isomorphism.lagda (99%) rename src/{ => plfa}/plta/Lambda.lagda (99%) rename src/{ => plfa}/plta/Lists.lagda (99%) rename src/{ => plfa}/plta/Modules.lagda (99%) rename src/{ => plfa}/plta/More.lagda (99%) rename src/{ => plfa}/plta/Naturals.lagda (99%) rename src/{ => plfa}/plta/Negation.lagda (99%) rename src/{ => plfa}/plta/Preface.lagda (98%) rename src/{ => plfa}/plta/Properties.lagda (99%) rename src/{ => plfa}/plta/Quantifiers.lagda (99%) rename src/{ => plfa}/plta/Relations.lagda (99%) rename src/{ => plfa}/plta/Statistics.lagda (95%) rename src/{ => plfa}/plta/Untyped.lagda (99%) diff --git a/Notes.md b/Notes.md index 78b8ff7c..e8099643 100644 --- a/Notes.md +++ b/Notes.md @@ -81,6 +81,11 @@ The following comments were collected on the Agda mailing list. - https://github.com/effectfully/random-stuff/blob/master/Normalization/Liftable.agda + also cites Abel's habilitation - http://www.cse.chalmers.se/~abela/habil.pdf + + See his note to the Agda mailing list of 26 June, + "Typed Jigger in vanilla Agda" + It points to the following solution. + - https://github.com/effectfully/random-stuff/blob/master/TypedJigger.agda + * András Kovács + applies unary parametricity diff --git a/_config.yml b/_config.yml index 68dd6a1a..14e4798a 100644 --- a/_config.yml +++ b/_config.yml @@ -1,6 +1,5 @@ title: > - Code the Infinite: - Programming Languages in Agda + Programming Language Foundations in Agda # the author field should not be used in the template author: Wen Kokke @@ -18,7 +17,7 @@ contributors: twitter_username: philipwadler description: > - Programming Languages in Agda. + Programming Language Foundations in Agda # include disqus to allow comments e.d. disqus: diff --git a/src/plta/Acknowledgements.lagda b/src/plfa/plta/Acknowledgements.lagda similarity index 100% rename from src/plta/Acknowledgements.lagda rename to src/plfa/plta/Acknowledgements.lagda diff --git a/src/plta/Bisimulation.lagda b/src/plfa/plta/Bisimulation.lagda similarity index 100% rename from src/plta/Bisimulation.lagda rename to src/plfa/plta/Bisimulation.lagda diff --git a/src/plta/Connectives.lagda b/src/plfa/plta/Connectives.lagda similarity index 99% rename from src/plta/Connectives.lagda rename to src/plfa/plta/Connectives.lagda index 5b45d5a3..688200c2 100644 --- a/src/plta/Connectives.lagda +++ b/src/plfa/plta/Connectives.lagda @@ -5,7 +5,7 @@ permalink : /Connectives/ --- \begin{code} -module plta.Connectives where +module plfa.Connectives where \end{code} This chapter introduces the basic logical connectives, by observing a diff --git a/src/plta/DeBruijn.lagda b/src/plfa/plta/DeBruijn.lagda similarity index 99% rename from src/plta/DeBruijn.lagda rename to src/plfa/plta/DeBruijn.lagda index 31511a8e..1c4df358 100644 --- a/src/plta/DeBruijn.lagda +++ b/src/plfa/plta/DeBruijn.lagda @@ -5,7 +5,7 @@ permalink : /DeBruijn/ --- \begin{code} -module plta.DeBruijn where +module plfa.DeBruijn where \end{code} The previous two chapters introduced lambda calculus, with a diff --git a/src/plta/Decidable.lagda b/src/plfa/plta/Decidable.lagda similarity index 99% rename from src/plta/Decidable.lagda rename to src/plfa/plta/Decidable.lagda index 07abe8a4..31efa52b 100644 --- a/src/plta/Decidable.lagda +++ b/src/plfa/plta/Decidable.lagda @@ -5,7 +5,7 @@ permalink : /Decidable/ --- \begin{code} -module plta.Decidable where +module plfa.Decidable where \end{code} We have a choice as to how to represent relations: diff --git a/src/plta/Equality.lagda b/src/plfa/plta/Equality.lagda similarity index 99% rename from src/plta/Equality.lagda rename to src/plfa/plta/Equality.lagda index 6efe0eb2..af0c70c4 100644 --- a/src/plta/Equality.lagda +++ b/src/plfa/plta/Equality.lagda @@ -5,7 +5,7 @@ permalink : /Equality/ --- \begin{code} -module plta.Equality where +module plfa.Equality where \end{code} Much of our reasoning has involved equality. Given two terms `M` diff --git a/src/plta/Fonts.lagda b/src/plfa/plta/Fonts.lagda similarity index 69% rename from src/plta/Fonts.lagda rename to src/plfa/plta/Fonts.lagda index e000bebf..dcb1b710 100644 --- a/src/plta/Fonts.lagda +++ b/src/plfa/plta/Fonts.lagda @@ -4,10 +4,6 @@ layout : page permalink : /Fonts/ --- -\begin{code} -module plta.Fonts where -\end{code} - Test page for fonts. All vertical bars should line up. \begin{code} @@ -17,7 +13,8 @@ abcdefghijklmnopqrstuvwxyz| ABCDEFGHIJKLMNOPQRSTUVWXYZ| ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ ʳˢᵗᵘᵛʷˣʸᶻ| ᴬᴮ ᴰᴱ ᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾ ᴿ ᵀᵁⱽᵂ | -ₐ ₑ ᵢⱼ ₒ ᵣ ᵤ ₓ | +ₐ ₑ ᵢⱼ ₒ ᵣₛₜᵤ ₓ | +𝔸𝔹ℂ𝔻𝔼𝔽𝔾ℍ𝕀𝕁𝕂𝕃𝕄ℕ𝕆ℙℚℝ𝕊𝕋𝕌𝕍𝕎𝕏𝕐ℤ| --------------------------| ----------| 0123456789| @@ -29,23 +26,42 @@ ABCDEFGHIJKLMNOPQRSTUVWXYZ| ΑΒΓΔΕΖΗΘΙΚΛΜΝΞΟΠΡΣΤΥΦΧΨΩ| ------------------------| ----| +ℕℕℕℕ| ∀∀∃∃| ƛƛ··| +′′″″| +‴‴⁗⁗| +††‡‡| +''""| +``~~| ≡≡≢≢| +≃≃≲≲| ≟≟≐≐| ⟨⟨⟩⟩| ⌊⌊⌋⌋| ⌈⌈⌉⌉| →→⇒⇒| ←←⇐⇐| -↦↦↠↠| +——↠↠| ∈∈∋∋| ⊢⊢⊣⊣| +∷∷∷∷| +⦂⦂⦂⦂| ----| -} \end{code} -Here are some characters that are not required to be monospaced. +Here are some characters that are exactly two spaces wide. +\begin{code} +{- +----| +😇😇| +😈😈| +----| +-} +\end{code} + +Here are some characters that are not used because they are not monospaced. \begin{code} {- diff --git a/src/plta/Induction.lagda b/src/plfa/plta/Induction.lagda similarity index 99% rename from src/plta/Induction.lagda rename to src/plfa/plta/Induction.lagda index af824eb4..debd5566 100644 --- a/src/plta/Induction.lagda +++ b/src/plfa/plta/Induction.lagda @@ -5,7 +5,7 @@ permalink : /Induction/ --- \begin{code} -module plta.Induction where +module plfa.Induction where \end{code} > Induction makes you feel guilty for getting something out of nothing diff --git a/src/plta/Inference.lagda b/src/plfa/plta/Inference.lagda similarity index 99% rename from src/plta/Inference.lagda rename to src/plfa/plta/Inference.lagda index 99d69df8..1c1f2443 100644 --- a/src/plta/Inference.lagda +++ b/src/plfa/plta/Inference.lagda @@ -5,7 +5,7 @@ permalink : /Inference/ --- \begin{code} -module plta.Inference where +module plfa.Inference where \end{code} diff --git a/src/plta/Isomorphism.lagda b/src/plfa/plta/Isomorphism.lagda similarity index 99% rename from src/plta/Isomorphism.lagda rename to src/plfa/plta/Isomorphism.lagda index dba6c9e1..dbcc55a7 100644 --- a/src/plta/Isomorphism.lagda +++ b/src/plfa/plta/Isomorphism.lagda @@ -5,7 +5,7 @@ permalink : /Isomorphism/ --- \begin{code} -module plta.Isomorphism where +module plfa.Isomorphism where \end{code} This section introduces isomorphism as a way of asserting that two diff --git a/src/plta/Lambda.lagda b/src/plfa/plta/Lambda.lagda similarity index 99% rename from src/plta/Lambda.lagda rename to src/plfa/plta/Lambda.lagda index 6c6fd62d..d14db290 100644 --- a/src/plta/Lambda.lagda +++ b/src/plfa/plta/Lambda.lagda @@ -7,7 +7,7 @@ permalink : /Lambda/ *Todo: Experiment with defining variable names* smart constructor `` ƛ`_⇒_ `` \begin{code} -module plta.Lambda where +module plfa.Lambda where \end{code}