diff --git a/src/Fonts.lagda b/src/Fonts.lagda new file mode 100644 index 00000000..08bd06a6 --- /dev/null +++ b/src/Fonts.lagda @@ -0,0 +1,58 @@ +--- +title : "Fonts" +layout : page +permalink : /Fonts +--- + +Test page for fonts. + +Agda: + +\begin{code} +{- +abcdefghijklmnopqrstuvwxyz +ABCDEFGHIJKLMNOPQRSTUVWXYZ +αβγδεφικλμνωπψρστυχξζ +ΑΒΓΔΕΦΙΚΛΜΝΩΠΨΡΣΤΥΧΞΖ +0123456789 +⁰¹²³⁴⁵⁶⁷⁸⁹ +₀₁₂₃₄₅₆₇₈₉ +𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛 +𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘 +------ +⟨⟨⟨⟩⟩⟩ +→→→⇒⇒⇒ +←←←⇐⇐⇐ +------ +------------ +⟶⟶⟶⟶ +⟹⟹⟹⟹ +------------ +⌊⌋⌈⌉ +---- +-} +\end{code} + +Indented code: + + abcdefghijklmnopqrstuvwxyz + ABCDEFGHIJKLMNOPQRSTUVWXYZ + αβγδεφικλμνωπψρστυχξζ + ΑΒΓΔΕΦΙΚΛΜΝΩΠΨΡΣΤΥΧΞΖ + 0123456789 + ⁰¹²³⁴⁵⁶⁷⁸⁹ + ₀₁₂₃₄₅₆₇₈₉ + 𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛 + 𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘 + ------ + ⟨⟨⟨⟩⟩⟩ + →→→⇒⇒⇒ + ←←←⇐⇐⇐ + ------ + ------------ + ⟶⟶⟶⟶ + ⟹⟹⟹⟹ + ------------ + ⌊⌋⌈⌉ + ---- +