LINUX.ORG.RU

История изменений

Исправление 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.[]))