小编Jas*_*ich的帖子

我正在尝试根据我在Haskell中编写的程序将一些指称语义编码到Agda中.

data Value = FunVal (Value -> Value)
           | PriVal Int
           | ConVal Id [Value]
           | Error  String

在阿格达,直接翻译将是;

data Value : Set where
    FunVal : (Value -> Value) -> Value
    PriVal : ? -> Value
    ConVal : String -> List Value -> Value
    Error  : String -> Value

但是我得到了与FunVal有关的错误,因为;

值并非严格为正,因为它出现在Value定义中构造函数FunVal类型中箭头的左侧.

这是什么意思？我可以用Agda编码吗？我是以错误的方式去做的吗？

谢谢.

我试图在Agda中证明一个简单的引理,我认为这是真的.

如果一个向量有两个以上的元素,那么采取head以下方法就init可以head立即采用它.

我的表述如下:

lem-headInit : ?{l} (xs : Vec ? (suc (suc l)))
                    -> head (init xs) ? head xs
lem-headInit (x ? xs) = ?

哪个给了我;

.l : ?
x  : ?
xs : Vec ? (suc .l)
------------------------------
Goal: head (init (x ? xs) | (initLast (x ? xs) | initLast xs)) ? x

作为回应.

我不完全了解如何阅读该(init (x ? xs) | (initLast (x ? xs) | initLast xs))组件.我想我的问题是; 是否有可能,该术语的含义和含义是什么.

非常感谢.