给定一个线性系统Ax = b,矩阵A和向量b具有整数值,我想找到解决这个方程的所有非负整数向量x.
到目前为止,我已经找到了一些技术,如Smith正规形式或Hermite正规形式的矩阵来找到整数解,我想我可以使用线性求解器来找到非负解.有没有一个可以让这更容易的图书馆？
Python解决方案是理想的,但如果一个库存在于另一种语言中我想知道它.
考虑以下（无效的）Agda 代码
data Example : Example ex ? Set where
ex : Example ex
这种类型可以通过以下方式在 Agda 中有效写入，利用 Agda 的特性，允许先给值类型，然后再定义
exampleex : Set
ex' : exampleex
data Example : exampleex ? Set where
ex : Example ex'
exampleex = Example ex'
ex' = ex
这一切都编译通过，Agda 正确地知道 ex : Example ex
但是，尝试使用模式匹配在 Example 之外定义函数会导致编译器崩溃
test : (e : Example ex) ? Example e ? ?
test ex x = 0
当我将此函数添加到文件中并运行“agda main.agda”时，agda 说“正在检查 main”但从未完成运行。Agda 中的类型检查不应该是可判定的吗？
另外，有没有办法解决这个问题并使测试功能可以定义？
当我写下以下函数是agda时,
f : (A : Set) ? (a : A) ? ?
f ? n = n
我希望错误说我没有指定所有情况.
相反,我收到此错误:
Type mismatch:
expected: ?
actual: ?
when checking that the expression n
has type ?
这里发生了什么？