publish Fonts

2018-05-23 15:46:13 -03:00 · 2018-05-23 15:46:13 -03:00 · c0dabd126d
commit c0dabd126d
parent 395419f79f
1 changed files with 58 additions and 0 deletions
--- a/src/Fonts.lagda
+++ 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
+    ⁰¹²³⁴⁵⁶⁷⁸⁹
+    ₀₁₂₃₄₅₆₇₈₉
+    𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛
+    𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘
+    ------
+    ⟨⟨⟨⟩⟩⟩
+    →→→⇒⇒⇒
+    ←←←⇐⇐⇐
+    ------
+    ------------
+    ⟶⟶⟶⟶
+    ⟹⟹⟹⟹
+    ------------
+    ⌊⌋⌈⌉
+    ----
+