deniok: (Default)
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 = _
Для того, чтобы правильно сделать коду на Агде грамотную синтаксическую раскраску, требуется не просто полноценно его распарсить, но ещё и повычислять изрядно по ходу дела. То есть ждать приличных внешних тулзов нечего, хочешь цветной Агды - сиди в emacs и не жужжи.

Между тем, хотелось бы (из педагогических, к примеру, соображений) иметь хорошо раскрашенный агдо-код для вставки куда угодно, и не в виде картинки. Отсюда вопрос - нельзя ли вытащить информацию о раскраске из emacs'а?

Я никому не скажу, что я большую часть времени работаю в Windows, поэтому мой вопрос относится в основном к этой OS, но если, например, это очень легко в какой другой OS, а в богомерзкой - очень сложно, то это была бы тоже полезная информация.

UPD1. Как нам сообщают умные люди в комментах можно:
(1) использовать саму Агду, она умеет генерировать правильно размеченный html:
agda --html --html-dir=<куда выводить> <корневой модуль>
(2) в emacs можно использовать htmlize (или htmlfontify, но у первого, вроде, настройки побогаче).

UPD2. Поправил цвета на в точности стандартные, а то некоторые ругаются.

Need help!

Dec. 14th, 2007 05:41 pm
deniok: (удивлён)
Друзья - меломаны!

Дочка на Новый Год затребовала себе колонки к своему компьтеру - музыку слушать. У нее стоит самая дешевая парочка, она ругается на звук. Посоветуйте что-нибудь в пределах тысяч двух-трёх.

Profile

deniok: (Default)
deniok

April 2017

S M T W T F S
      1
23 45678
9101112131415
16171819202122
23242526272829
30      

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 22nd, 2017 10:18 pm
Powered by Dreamwidth Studios