Closed
Description
@TOTBWF reports:
Found a case splitting bug
proofs :: forall ext err s m goal. (MonadExtract ext m) => s -> ProofStateT ext ext err s m goal -> m [Either err (ext, s, [goal])]
proofs s p = go s [] pure p
where
go :: s -> [goal] -> (goal' -> ProofStateT ext ext err s m goal) -> ProofStateT ext ext err s m goal' -> m [Either err (ext, s, [goal])]
go s goals cont p1 = _
splitting on p1
causes this
proofs :: forall ext err s m goal. (MonadExtract ext m) => s -> ProofStateT ext ext err s m goal -> m [Either err (ext, s, [goal])]
proofs s p = _
proofs s p = _
proofs s p = _
proofs s p = _
proofs s p = _
proofs s p = _
proofs s p = _
proofs s p = _
proofs s p = _