Об умножение

[deniok]

Эти ваши интернеты бурлят:

ru-marazm.livejournal.com/3591670.html

lj.rossia.org/users/tiphareth/1685303.html

Агда, кстати, на стороне внучки, 9 раз по 2 литра будет 9 * 2:

_*_ : ℕ → ℕ → ℕ
zero  * n = zero
suc m * n = n + (m * n)

Впрочем внучке стоило бы снять все вопросы, предоставив доказательство

*-commutative : ∀ m n → m * n ≡ n * m

Взяв его, например, из Data.Nat.Properties. Или получив самостоятельно.

Comments

[sassa_nf]

А я получаю вот такое:

An internal error has occurred. Please report this as a bug.
Location of the error: src/full\Agda\Interaction\GhciTop.hs:646

Это вообще известно как бороть?

(C-c C-l в емаксе)

[deniok]

Модуль, например, не надо называть Test :)
(это я описываю тот случай, когда получал нечто подобное)

[sassa_nf]

хахаха, :) файл на виндовз начинался с маленькой буквы. Вышел из емакса, переименовал с большой буквой - все дела :)