小编nob*_*ody的帖子

我的证明脚本给了我愚蠢的类型平等,nat = bool或者 nat = list unit我需要用来解决相互矛盾的目标.

在正常的数学中,这将是微不足道的.鉴于集合bool := { true, false }, nat := { 0, 1, 2, ... }我知道true ? bool,但是true ? nat,因此bool ? nat.在Coq,我甚至不知道如何陈述true :? nat.

题

有没有办法证明这些平等是错误的？或许,这不可能吗？

(编辑:删除了一长串失败的attemts,仍然可以在历史上看到.)

我有一种方法可以从 lua 中的父列表指针构建树。特别是我有这个lua 表

parents = {2,3,13,5,12,7,11,9,10,11,12,13,14,0}

连同两个功能：

函数 1（创建节点）：

function create_node(parent, i, created, root)
  if created[i] ~= nil then
        return
  end
    print(i)
--    print(parent)
--  Create a new node and set created[i]
    local new_node = Tree()
    new_node.idx = i
    created[i] = new_node


--    If 'i' is root, change root pointer and return
    if parent[i] == 0 then
       root[1] = created[i] -- root[1] denotes root of the tree

       return
    end

--    If parent is not created, then create parent …