Coq/underdefined中的部分功能？

我一直在尝试使用Concrete Semantics(为Coq Isabelle/HOL 编写)作为参考点来编写和验证Agda中的编译器.我正在为该文本中使用的相同语言定义编译.

对于上下文,我已经完成了编译器的编写,现在我处于验证阶段,但是我必须在机器指令执行的定义中对Concrete Semantics做出重大改变.这种差异似乎在Agda中是必要的,但现在使验证阶段非常复杂.

在尝试使用Concrete Semantics中给出的更简单的指令执行版本时,我遇到了这一行,这可以解释为什么我无法直接将其转换为Agda:

列表的头部,第一个元素和尾部,列表的其余部分也很有用:

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

请注意,由于HOL是总函数的​​逻辑,hd []因此定义了,但我们不知道结果是什么.也就是说,hd []未定义但未定义.

hd []欠定义是什么意思？这相当于在Agda中使用不完整的模式吗？

汇编指令执行函数在很大程度上依赖于hd.在我在Agda中的实现中,我给了多个类型的索引,以允许我构建堆栈总是具有最小元素数量的证明,以避免不完整的模式匹配问题.现在我正在尝试验证编译器,证明的大小比具体语义中的证明更复杂,因为我必须使用这些索引.

我是否遗漏了某些东西,或者具体语义中的证据是不完整的,hd []未被定义？