История изменений
Исправление
Unununij,
(текущая версия)
:
Хм, а в Agda всё нормально с unicode
module HelloWorld where
open import IO
main = putStr "Привет, мир!"
.IO.♯-16
('П' .Data.Colist.Colist.∷
.Data.Colist.♯-2 'П'
('р' .Agda.Builtin.List.List.∷
'и' .Agda.Builtin.List.List.∷
'в' .Agda.Builtin.List.List.∷
'е' .Agda.Builtin.List.List.∷
'т' .Agda.Builtin.List.List.∷
',' .Agda.Builtin.List.List.∷
' ' .Agda.Builtin.List.List.∷
'м' .Agda.Builtin.List.List.∷
'и' .Agda.Builtin.List.List.∷
'р' .Agda.Builtin.List.List.∷
'!' .Agda.Builtin.List.List.∷ .Agda.Builtin.List.List.[]))
Исходная версия
Unununij,
:
Хм, а в Agda всё нормально с unicode
module HelloWorld where
open import IO
main = putStr "Привет, мир!"
.IO.♯-16
('П' .Data.Colist.Colist.∷
.Data.Colist.♯-2 'П'
('р' .Agda.Builtin.List.List.∷
'и' .Agda.Builtin.List.List.∷
'в' .Agda.Builtin.List.List.∷
'е' .Agda.Builtin.List.List.∷
'т' .Agda.Builtin.List.List.∷
',' .Agda.Builtin.List.List.∷
' ' .Agda.Builtin.List.List.∷
'м' .Agda.Builtin.List.List.∷
'и' .Agda.Builtin.List.List.∷
'р' .Agda.Builtin.List.List.∷
'!' .Agda.Builtin.List.List.∷ .Agda.Builtin.List.List.[]))
[quote][quote][br][/quote][/quote].IO.♯-18
('П' .Data.Colist.Colist.∷
.Data.Colist.♯-2 'П'
('р' .Agda.Builtin.List.List.∷
'и' .Agda.Builtin.List.List.∷
'в' .Agda.Builtin.List.List.∷
'е' .Agda.Builtin.List.List.∷
'т' .Agda.Builtin.List.List.∷
',' .Agda.Builtin.List.List.∷
' ' .Agda.Builtin.List.List.∷
'м' .Agda.Builtin.List.List.∷
'и' .Agda.Builtin.List.List.∷
'р' .Agda.Builtin.List.List.∷
'!' .Agda.Builtin.List.List.∷ .Agda.Builtin.List.List.[]))