From e819aee20aa7ac2a57c357b239a74fe35196c1a8 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Tue, 26 Jun 2018 15:01:29 +0100 Subject: [PATCH] Simplified plta.Fonts page --- src/plta/Fonts.lagda | 51 +++++++++----------------------------------- 1 file changed, 10 insertions(+), 41 deletions(-) diff --git a/src/plta/Fonts.lagda b/src/plta/Fonts.lagda index f0f6191a..9e614ca4 100644 --- a/src/plta/Fonts.lagda +++ b/src/plta/Fonts.lagda @@ -10,8 +10,6 @@ module plta.Fonts where Test page for fonts. All vertical bars should line up. -Agda: - \begin{code} {- abcdefghijklmnopqrstuvwxyz| @@ -19,15 +17,19 @@ ABCDEFGHIJKLMNOPQRSTUVWXYZ| ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ ʳˢᵗᵘᵛʷˣʸᶻ| ᴬᴮ ᴰᴱ ᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾ ᴿ ᵀᵁⱽᵂ | ₐ ₑ ᵢⱼ ₒ ᵣ ᵤ ₓ | + αβγδεφικλμνωπψρστυχξζ| ΑΒΓΔΕΦΙΚΛΜΝΩΠΨΡΣΤΥΧΞΖ| + 0123456789| ⁰¹²³⁴⁵⁶⁷⁸⁹| ₀₁₂₃₄₅₆₇₈₉| + ⟨⟨⟨⟩⟩⟩| →→→⇒⇒⇒| ←←←⇐⇐⇐| ------| + ⌊⌋⌈⌉| →→→→| ↦↦↦↦| @@ -37,44 +39,11 @@ ABCDEFGHIJKLMNOPQRSTUVWXYZ| ∈∈∈∈| ∋∋∋∋| ----| ------------- -⟶⟶⟶⟶ -⟹⟹⟹⟹ ------------- -𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛 -𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘 + +⟶⟶⟶⟶| +⟹⟹⟹⟹| + +𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛| +𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘| -} \end{code} - -Indented code: - - abcdefghijklmnopqrstuvwxyz| - ABCDEFGHIJKLMNOPQRSTUVWXYZ| - ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ ʳˢᵗᵘᵛʷˣʸᶻ| - ᴬᴮ ᴰᴱ ᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾ ᴿ ᵀᵁⱽᵂ | - ₐ ₑ ᵢⱼ ₒ ᵣ ᵤ ₓ | - αβγδεφικλμνωπψρστυχξζ| - ΑΒΓΔΕΦΙΚΛΜΝΩΠΨΡΣΤΥΧΞΖ| - 0123456789| - ⁰¹²³⁴⁵⁶⁷⁸⁹| - ₀₁₂₃₄₅₆₇₈₉| - ⟨⟨⟨⟩⟩⟩| - →→→⇒⇒⇒| - ←←←⇐⇐⇐| - ------| - ⌊⌋⌈⌉| - →→→→| - ↦↦↦↦| - ↠↠↠↠| - ⊢⊢⊢⊢| - ⊣⊣⊣⊣| - ∈∈∈∈| - ∋∋∋∋| - ----| - ------------ - ⟶⟶⟶⟶ - ⟹⟹⟹⟹ - ------------ - 𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛 - 𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘 -