updated font test page

This commit is contained in:
wadler 2018-06-26 10:26:47 -03:00
parent ffbc3ffb2b
commit 1882ea9e36

View file

@ -8,7 +8,7 @@ permalink : /Fonts/
module plta.Fonts where
\end{code}
Test page for fonts.
Test page for fonts. All vertical bars should line up.
Agda:
@ -24,27 +24,25 @@ ABCDEFGHIJKLMNOPQRSTUVWXYZ|
0123456789|
⁰¹²³⁴⁵⁶⁷⁸⁹|
₀₁₂₃₄₅₆₇₈₉|
𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛
𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘
------
⟨⟨⟨⟩⟩⟩
→→→⇒⇒⇒
←←←⇐⇐⇐
------
⟨⟨⟨⟩⟩⟩|
→→→⇒⇒⇒|
←←←⇐⇐⇐|
------|
⌊⌋⌈⌉|
→→→→|
↦↦↦↦|
↠↠↠↠|
⊢⊢⊢⊢|
⊣⊣⊣⊣|
∈∈∈∈|
∋∋∋∋|
----|
------------
⟶⟶⟶⟶
⟹⟹⟹⟹
------------
⌊⌋⌈⌉
----
→→→→
↦↦↦↦
↠↠↠↠
⊢⊢⊢⊢
⊣⊣⊣⊣
∈∈∈∈
∋∋∋∋
----
𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛
𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘
-}
\end{code}
@ -60,24 +58,23 @@ Indented code:
0123456789|
⁰¹²³⁴⁵⁶⁷⁸⁹|
₀₁₂₃₄₅₆₇₈₉|
𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛
𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘
------
⟨⟨⟨⟩⟩⟩
→→→⇒⇒⇒
←←←⇐⇐⇐
------
⟨⟨⟨⟩⟩⟩|
→→→⇒⇒⇒|
←←←⇐⇐⇐|
------|
⌊⌋⌈⌉|
→→→→|
↦↦↦↦|
↠↠↠↠|
⊢⊢⊢⊢|
⊣⊣⊣⊣|
∈∈∈∈|
∋∋∋∋|
----|
------------
⟶⟶⟶⟶
⟹⟹⟹⟹
------------
⌊⌋⌈⌉
----
→→→→
↦↦↦↦
↠↠↠↠
⊢⊢⊢⊢
⊣⊣⊣⊣
∈∈∈∈
∋∋∋∋
----
𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛
𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘