以下是一个使用Agda编写的函数,该函数返回一个列表的最后一个元素:
open import Data.List
lastElem : {A : Set} → List A → Maybe A
lastElem [] = nothing
lastElem (x ∷ []) = just x
lastElem (x ∷ xs) = lastElem xs
在上面的代码中,我们使用了Agda的Data.List
模块,它提供了与列表相关的函数和数据类型。函数lastElem
接受一个类型为List A
的列表作为参数,并返回一个Maybe A
类型的值,表示可能存在或不存在最后一个元素。
函数使用模式匹配来处理不同的情况。当列表为空时,我们返回nothing
表示没有最后一个元素。当列表只有一个元素时,我们将这个元素包装在just
中返回。对于其他情况,我们递归调用lastElem
函数来处理剩余的列表。
这个函数的类型签名中的{A : Set}
表示我们可以在调用时显式地传递类型参数,也可以根据上下文自动推断出类型参数。