相关疑难解决方法(0)

这种So类型的目的是什么？音译到Agda:

data So : Bool ? Set where
  oh : So true

So将布尔命题提升为逻辑命题.Oury和Swierstra的介绍性论文"Pi的力量"给出了一个由表格列索引的关系代数的例子.取两个表的产品要求它们具有不同的列,他们使用这些列So:

Schema = List (String × U)  -- U is the universe of SQL types

-- false iff the schemas share any column names
disjoint : Schema -> Schema -> Bool
disjoint = ...

data RA : Schema ? Set where
  -- ...
  Product : ? {s s'} ? {So (disjoint s s')} ? RA s ? RA s' ? RA …

假设我们定义了一个函数

f : N \to N
f 0 = 0
f (s n) = f (n/2) -- this / operator is implemented as floored division.

Agda将在三文鱼中绘制f,因为它无法判断n/2是否小于n.我不知道怎么告诉Agda的终止检查器.我在标准库中看到它们有一个2的分区和n/2 <n的证明.但是,我仍然没有看到如何让终止检查器意识到已经在较小的子问题上进行了递归.

我想写一个以set为输入的函数,return true if it is top and false if it is bottom. 我试过这种方式..

isTop : Set ? Bool
isTop x = if (x eq ?) then true
              else false

但我无法正确定义eq.我试过......

_eq_ : Set ? Set ? Bool
? eq ? = false

这不起作用,因为当我检查 T eq T it is also returning false.

请帮我写这个eq函数或任何其他写isTop的方法.