小编Ash*_*ley的帖子

假设我有三个自己的包,AB&C,依赖于Hackage中的许多其他包.我正在使用cabal 1.18.

• C取决于A和B.
• B取决于A.
• A&B有测试套件.

我像这样设置了沙箱:

cd /path/to/sandbox
cabal sandbox init
cabal sandbox add-source /path/to/A
cabal sandbox add-source /path/to/B
cabal sandbox add-source /path/to/C

我想构建所有包,在我的包上运行所有测试套件,但不运行依赖包,显示完整的测试输出.最好的方法是什么？

选项1

cd /path/to/sandbox
cabal install --enable-tests A B C

问题:

• 没有办法传递--show-details=always给cabal install.
• 测试输出隐藏在日志文件中,未显示.
• 如果用户碰巧cabal install A先前做了,A将不会重建,测试将无法运行.

选项2

cd /path/to/A
cabal sandbox init --sandbox=/path/to/sandbox/.cabal-sandbox
cd /path/to/B
cabal sandbox init --sandbox=/path/to/sandbox/.cabal-sandbox

cd /path/to/A
cabal configure --enable-tests
cabal test --show-details=always
cd /path/to/B
cabal configure --enable-tests
cabal test --show-details=always
cabal install C

问题:

• 这会导致A和B库被不必要地重建. …

如何在Coq中展开类实例？似乎只有在实例不包含证明或其他内容时才有可能.考虑一下:

Class C1 (t:Type) := {v1:t}.
Class C2 (t:Type) := {v2:t;c2:v2=v2}.

Instance C1_nat: C1 nat:= {v1:=4}.

Instance C2_nat: C2 nat:= {v2:=4}.
trivial.
Qed.

Theorem thm1 : v1=4.
unfold v1.
unfold C1_nat.
trivial.
Qed.

Theorem thm2 : v2=4.
unfold v2.
unfold C2_nat.
trivial.
Qed.

thm1证明了,但我无法证明thm2; 它在unfold C2_nat步骤中抱怨Error: Cannot coerce C2_nat to an evaluable reference..

这是怎么回事？我如何得到C2_nat定义v2？

在Coq中，当试图证明记录相等时，是否有一种策略可以将其分解为所有字段相等？例如，

Record R := {x:nat;y:nat}.

Variables a b c d : nat.

Lemma eqr : {|x:=a;y:=b|} = {|x:=c;y:=d|}.

有没有一种策略可以将其减少到a = c /\ b = d？请注意，一般而言，任何一个a b c d可能都是复杂的大型证明术语（然后我可以使用证明不相关公理来执行）。

我尝试了这个：

{-# LANGUAGE TypeFamilyDependencies #-}
module Injective where

type family F (a :: *) = (fa :: *) | fa -> a

convert :: F a ~ F b => a -> b
convert x = x

GHC 8.6.4给了我这个错误

    • Could not deduce: a ~ b
      from the context: F a ~ F b
        bound by the type signature for:
                   convert :: forall a b. (F a ~ F b) => a -> b
        at Injective.hs:6:1-30

为什么？当然，单射性的全部要点是可以从中推论a …