Неполная функция в Coq / недоопределена?

Я пытался написать и проверить компилятор в Agda, используя Конкретная семантика (который написан для Coq Isabelle / HOL) в качестве ориентира. Я определяю компиляцию для тех же языков, которые используются в этом тексте.

Что касается контекста, я закончил писать компилятор и сейчас нахожусь на стадии проверки, однако мне пришлось существенно изменить конкретную семантику в определении выполнения машинных инструкций. Это различие казалось необходимым в Agda, но теперь этап проверки становится невероятно сложным.

Пытаясь выполнить более простую версию выполнения инструкций, приведенную в Конкретной семантике, я наткнулся на эту строку, которая может объяснить, почему у меня возникли проблемы с прямым переводом ее в Agda:

Also useful are the head of a list, its first element, and the tail, the rest of the list:

fun hd :: 'a list ⇒ 'a
hd (x # xs) = x

Note that since HOL is a logic of total functions, hd [] is defined, but we do not know what the result is. That is, hd [] is not undefined but underdefined.

Что значит недооценка hd []? Это эквивалент неполного шаблона в Agda?

Функция выполнения инструкций сборки сильно зависит от hd. В моей реализации этого в Agda я дал индексы для нескольких типов, чтобы позволить мне построить доказательства того, что стек всегда имеет минимальное количество элементов, чтобы избежать проблемы неполного сопоставления с образцом. Теперь, когда я пытаюсь проверить компилятор, доказательства намного сложнее, чем доказательства в Конкретной семантике, поскольку мне приходится работать с этими индексами.

Я что-то упустил или доказательства в Concrete Semantics неполны, а hd [] не определен?