Рабочий момент, Agda

[deniok]

Что-то у меня хаскелевский импорт вот так работает

{-# IMPORT System.IO #-}

а вот так ломается

{-# IMPORT System.IO (hPutStrLn) #-}

говоря Parse error (hPutStrLn). Хотя у Норелла в Dependently Typed Programming in Agda список импорта в примере используется. Agda 2.3.0.1 под Windows. Посмотрите у кого более свежая (2.3.2) и/или другая OS.

Comments

[deni-ok.livejournal.com]

Да? Это плохо. Может Лев (ау, lionet) что-то придумает.

А вы связывались с Нореллом по этому поводу?

[oxij.livejournal.com]

Я меншонил его в твитторе по этому поводу, но он не отреагировал, и я решил не продолжать.

[deni-ok.livejournal.com]

Ну поскольку моя цель скорее культуртрегерская, то в крайнем случае выложу полуанонимно.