Merge pull request #569 from Altariarite/Fonts.lagda.md

changed codeblocks to displays in Fonts.lagda.md

src/plfa/backmatter/Fonts.lagda.md

@@ -11,113 +11,101 @@ module plfa.backmatter.Fonts where
 
 Preferably, all vertical bars should line up.
 
-```
+    --------------------------|
-{-
+    abcdefghijklmnopqrstuvwxyz|
---------------------------|
+    ABCDEFGHIJKLMNOPQRSTUVWXYZ|
-abcdefghijklmnopqrstuvwxyz|
+    ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ ʳˢᵗᵘᵛʷˣʸᶻ|
-ABCDEFGHIJKLMNOPQRSTUVWXYZ|
+    ᴬᴮ ᴰᴱ ᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾ ᴿ ᵀᵁⱽᵂ   |
-ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ ʳˢᵗᵘᵛʷˣʸᶻ|
+    ₐ   ₑ  ₕᵢⱼₖₗₘₙₒₚ ᵣₛₜᵤ  ₓ  |
-ᴬᴮ ᴰᴱ ᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾ ᴿ ᵀᵁⱽᵂ   |
+    --------------------------|
-ₐ   ₑ  ₕᵢⱼₖₗₘₙₒₚ ᵣₛₜᵤ  ₓ  |
+    ----------|
---------------------------|
+    0123456789|
-----------|
+    ⁰¹²³⁴⁵⁶⁷⁸⁹|
-0123456789|
+    ₀₁₂₃₄₅₆₇₈₉|
-⁰¹²³⁴⁵⁶⁷⁸⁹|
+    ----------|
-₀₁₂₃₄₅₆₇₈₉|
+    ------------------------|
-----------|
+    αβγδεζηθικλμνξοπρστυφχψω|
-------------------------|
+    ΑΒΓΔΕΖΗΘΙΚΛΜΝΞΟΠΡΣΤΥΦΧΨΩ|
-αβγδεζηθικλμνξοπρστυφχψω|
+    ------------------------|
-ΑΒΓΔΕΖΗΘΙΚΛΜΝΞΟΠΡΣΤΥΦΧΨΩ|
+    ----|
-------------------------|
+    ≠≠≠≠|
-----|
+    ηημμ|
-≠≠≠≠|
+    ΓΓΔΔ|
-ηημμ|
+    ΣΣΠΠ|
-ΓΓΔΔ|
+    λλλλ|
-ΣΣΠΠ|
+    ƛƛƛƛ|
-λλλλ|
+    ····|
-ƛƛƛƛ|
+    ××××|
-····|
+    ℓℓℓℓ|
-××××|
+    ≡≡≡≡|
-ℓℓℓℓ|
+    ¬¬¬¬|
-≡≡≡≡|
+    ≤≤≥≥|
-¬¬¬¬|
+    ∅∅∅∅|
-≤≤≥≥|
+    ————|
-∅∅∅∅|
+    ††‡‡|
-————|
+    ^^^^|
-††‡‡|
+    ''""|
-^^^^|
+    ``~~|
-''""|
+    ⊎⊎⊃⊃|
-``~~|
+    ∧∧∨∨|
-⊎⊎⊃⊃|
+    ⊗⊗⊗⊗|
-∧∧∨∨|
+    ⊔⊔⊔⊔|
-⊗⊗⊗⊗|
+    cᶜbᵇ|
-⊔⊔⊔⊔|
+    lˡrʳ|
-cᶜbᵇ|
+    ⁻⁻⁺⁺|
-lˡrʳ|
+    ℕℕℕℕ|
-⁻⁻⁺⁺|
+    ∀∀∃∃|
-ℕℕℕℕ|
+    ′′″″|
-∀∀∃∃|
+    ∘∘∘∘|
-′′″″|
+    ‌≢≢≃≃|
-∘∘∘∘|
+    ≲≲≳≳|
-‌≢≢≃≃|
+    ≟≟≐≐|
-≲≲≳≳|
+    ∸∸∸∸|
-≟≟≐≐|
+    ⟨⟨⟩⟩|
-∸∸∸∸|
+    ⌊⌊⌋⌋|
-⟨⟨⟩⟩|
+    ⌈⌈⌉⌉|
-⌊⌊⌋⌋|
+    ↑↑↓↓|
-⌈⌈⌉⌉|
+    ⇔⇔↔↔|
-↑↑↓↓|
+    →→⇒⇒|
-⇔⇔↔↔|
+    ←←⇐⇐|
-→→⇒⇒|
+    ↞↞↠↠|
-←←⇐⇐|
+    ∈∈∋∋|
-↞↞↠↠|
+    ⊢⊢⊣⊣|
-∈∈∋∋|
+    ⊥⊥⊤⊤|
-⊢⊢⊣⊣|
+    ∷∷∷∷|
-⊥⊥⊤⊤|
+    ∎∎∎∎|
-∷∷∷∷|
+    ⦂⦂⦂⦂|
-∎∎∎∎|
+    ∥∥∥∥|
-⦂⦂⦂⦂|
+    ★★★★|
-∥∥∥∥|
+    ∌∌∉∉|
-★★★★|
+    ⨟⨟⨟⨟|
-∌∌∉∉|
+    ⨆⨆⨆⨆|
-⨟⨟⨟⨟|
+    〔〔〕〕|
-⨆⨆⨆⨆|
+    ----|
-〔〔〕〕|
-----|
--}
-```
 
 In the book we use the em-dash to make big arrows.
 
-```
+    ----|
-{-
+    —→—→|
-----|
+    ←—←—|
-—→—→|
+    ↞—↞—|
-←—←—|
+    —↠—↠|
-↞—↞—|
+    ----|
-—↠—↠|
-----|
--}
-```
 
 Here are some characters that are often not monospaced.
 
-```
+    ----|
-{-
+    😇😇|
-----|
+    😈😈|
-😇😇|
+    ⁗⁗|
-😈😈|
+    ‴‴|
-⁗⁗|
+    ----|
-‴‴|
+    ------------|
-----|
+    ------------|
-------------|
+    ----------|
-------------|
+    𝔸𝔹𝔻𝔼𝔽𝔾𝕀𝕁𝕂𝕃𝕄ℕ𝕆𝕊|
-----------|
+    𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛|
-𝔸𝔹𝔻𝔼𝔽𝔾𝕀𝕁𝕂𝕃𝕄ℕ𝕆𝕊|
+    𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘|
-𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛|
+    ℰℱ|
-𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘|
+    ----------|
-ℰℱ|
-----------|
 
--}
-```