Что-то у меня хаскелевский импорт вот так работает
{-# 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.

open import Data.Nat

data Fin : ℕ → Set where
fzero : {n : ℕ} → Fin (suc n)
fsuc : {n : ℕ} → Fin n → Fin (suc n)

magic₁ : {A : Set} → Fin zero → A
magic₁ ()

magic₂ : {A : Set} → Fin zero → A
magic₂ n = _
Для того, чтобы правильно сделать коду на Агде грамотную синтаксическую раскраску, требуется не просто полноценно его распарсить, но ещё и ( Read more... )

Оказывается, абсурдный образец не обязателен (хотя и часто полезен) при отсутствии допустимых образцов конструктора:

module AbsurdTest where ( Read more... )

на почве русской Википедии. Вот плод:

http://ru.wikipedia.org/wiki/Agda

Улучшайте при желании, не ухудшайте без особой нужды.

Напоминаю, что очередная встреча SPbHUG, которую теперь зовут FProg, пройдёт в четверг, 12 июля в 19:00 в офисе компании Яндекс. Предполагается, что нашему вниманию будут предложены следующие доклады:

• Jan Malakhovski Введение в Agda.
• Evgeny Kotelnikov Зависимые типы в Haskell.
• Andrey Vlasovskikh Команда spb-archlinux на ICFP Contest 2009.

Подробная ( Read more... )