代码之家  ›  专栏  ›  技术社区  ›  Yang Bo

如何在Idris REPL中创建空列表?

  •  2
  • Yang Bo  · 技术社区  · 6 年前

    myEmptyList myNonemptyList 我的空列表

         ____    __     _                                          
        /  _/___/ /____(_)____                                     
        / // __  / ___/ / ___/     Version 1.3.0
      _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
     /___/\__,_/_/  /_/____/       Type :? for help               
    
    Idris is free software with ABSOLUTELY NO WARRANTY.            
    For details type :warranty.
    Idris> :let myEmptyList : List Integer = []
    (input):1:33: When checking type of myEmptyList:
    When checking argument y to type constructor =:
            Type mismatch between
                    List elem (Type of [])
            and
                    Type (Expected type)
    (input):1:18:No type declaration for myEmptyList
    Idris> :let myNonemptyList : List Integer = [42]
    
    1 回复  |  直到 6 年前
        1
  •  4
  •   András Kovács    6 年前

    不匹配是因为 :let myEmptyList : List Integer = [] myEmptyList ,它仅将其类型声明为 List Integer = [] ,是一个相等类型,由于 [] List Integer 有不同的类型。

    你可以定义 具体如下: :let myEmptyList : List Integer; myEmptyList = [] ,或者 :let myEmptyList = the (List Integer) [] .