In automated theorem proving (proof search), I compose transformers of type
t :: Claim -> IO (Maybe (Claim, Proof -> Proof))
such that: when t c
returns Just (c', f)
, then c'
implies c
and a proof for c
is obtained from a proof p'
for c'
by computing f p'
.
Is this a lens, somehow? (If yes, what would it help?)
There's also a more general case (for several, or zero, subgoals)
ts :: Claim -> IO (Maybe ([Claim], [Proof] -> Proof))
The IO
part is important because these transformers do substantial work (calling external processes), and I might want to impose timeouts.