Agda, абсурд в образцах

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

module AbsurdTest where

data   False : Set where -- необитаемый
record True  : Set where -- синглетон

data Bool : Set where
  true  : Bool
  false : Bool

-- декодирующая функция для булева универсума
isTrue : Bool → Set
isTrue true  = True
isTrue false = False

not_ : Bool → Bool
not true  = false
not false = true

-- абсурдистская версия
lem-not²≡id₁ : (a : Bool) → isTrue (not not a) → isTrue a
lem-not²≡id₁ true p = p
lem-not²≡id₁ false ()

-- обывательская версия
lem-not²≡id₂ : (a : Bool) → isTrue (not not a) → isTrue a
lem-not²≡id₂ true  p = p
lem-not²≡id₂ false p = p

Во второй версии во втором клозе мы спокойно пишем p, хотя его тип isTrue (not not false) редуцируется к необитаемому False.

С каноническим примером такое не пройдёт

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 = {! !}

Если здесь в дырку в magic₂ засунуть _, то нам покрасят его жёлтым, сигнализируя тем самым, что подходящей метапеременной Агде тут не вывести.

Agda, вопрос о подсветке синтаксиса

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. Поправил цвета на в точности стандартные, а то некоторые ругаются.