subscript numbers are no longer special
This commit is contained in:
parent
580fbc8fd8
commit
f58fa5218f
2 changed files with 0 additions and 19 deletions
|
@ -30,14 +30,6 @@ BTelescope : Nat -> Nat -> Type
|
|||
BTelescope = Telescope' BindName
|
||||
|
||||
|
||||
private
|
||||
subscript : String -> String
|
||||
subscript = pack . map sub . unpack where
|
||||
sub : Char -> Char
|
||||
sub c = case c of
|
||||
'0' => '₀'; '1' => '₁'; '2' => '₂'; '3' => '₃'; '4' => '₄'
|
||||
'5' => '₅'; '6' => '₆'; '7' => '₇'; '8' => '₈'; '9' => '₉'; _ => c
|
||||
|
||||
private
|
||||
superscript : String -> String
|
||||
superscript = pack . map sup . unpack where
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue