在自动定理证明(证明搜索)中,我组成了类型的转化器。
t :: Claim -> IO (Maybe (Claim, Proof -> Proof))
这里的意思是:当 t c
返回 Just (c', f)
时,c'
意味着 c
,并且可以通过计算 f p'
来从证明 p'
获得证明 c
。
这是一个镜头吗?(如果是,它有什么帮助吗?)
还有一个更一般的情况(适用于多个或零个子目标)
ts :: Claim -> IO (Maybe ([Claim], [Proof] -> Proof))
IO
部分非常重要,因为这些转换器会执行大量的工作(调用外部进程),我可能需要设置超时。