小编pha*_*dej的帖子

如果我有两个镜头:

foo :: Lens' X Foo
bar :: Lens' X Bar

有没有办法构建产品镜头:

foobar :: Lens' X (Foo, Bar)
foobar = ... foo bar 

还是不可能？

我决定尝试给堆叠一次.我安装了它并用它来安装最新版本的ghc.我已经使用堆栈来安装一些软件包,但ghc看不到软件包,当我用ghc-pkg列出软件包时,我看到我通过堆栈安装的软件包不在那里.为什么是这样？我是否误解了堆栈的目的？

是否有一些内置功能或插件可以用于获取lein控制台,因此例如可以在不等待JVM启动的情况下进行测试.

$ lein console
>>> test
...
>>> test
...
>>> jar

注意:我想自己触发测试运行,而不是通过观察源文件.这就是为什么我想要一个lein控制台.

澄清:我不是在寻找lein repl.我想有一个控制台,我可以运行lein任务命令.

我需要一个更多的引理来证明这inj? x ? inj? y是荒谬的,作为关于?Agda中不相交联合类型()的更大定理的一部分.

这个结果将直接来自两个构造函数?,即inj?和inj?不相交.那是阿格达的情况吗？我该如何证明？

这是完整的引理:

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Sum


lemma : ? {a b} {A : Set a} {B : Set b} {x : A} {y : B} ? ¬ inj? x ? inj? y
lemma eq = ?

据我所知,我们可以实现MonadReader s (StateT s m)实例:

instance MonadReader s (StateT s m) where
    ask = get
    local f m = do
        s <- get
        put (f s)
        m
        put s   

即为什么不是

class MonadReader s m => MonadState s m | s -> m where ...

同样,我们可以有Monoid s => MonadWriter s (StateT s m)实例.

选择之间有一些深层次的原因吗？

这个问题是由动机是否MonadError与MonadWriter应是超类MonadChronicle

与.gitignore：

foo/

以及一个git仓库：

./quux
./quux/foo
./quux/foo/bar
./quux/foo/bar/baz

作为foo被忽略，git的假设工作目录是干净的：

% git status
# On branch master
nothing to commit, working directory clean

在git clean -ndx打印：

% git clean -ndx
Would remove quux/

但是git clean -ndX什么也不打印。我希望它也会删除quux/。

这是我没有得到的错误还是某些gitignore功能？如果我添加一些文件quux并提交。比git clean会尝试quux/foo/按预期删除。

我的Git是很新：git version 1.8.3.4。

我发现了一个方便的功能:

coerce : ? {?} {A B : Set ?} ? A ? B ? A ? B
coerce refl x = x

在使用索引类型定义函数时.在索引在定义上不相等的情况下,i,e,必须使用引理来显示类型匹配.

zipVec : ? {a b n m } {A : Set a} {B : Set b} ? Vec A n ? Vec B m ? Vec (A × B) (n ? m)
zipVec [] _ = []
zipVec {n = n} _ [] = coerce (cong (Vec _) (0?n?0 n)) []
zipVec (x ? xs) (y …