Lava.Vis

Documentation

vis :: Checkable a => a -> IO ProofResult

writeVis :: (Constructive a, Generic b) => String -> (a -> b) -> IO ()

writeVisInput :: (Generic a, Generic b) => String -> (a -> b) -> a -> IO ()

writeVisInputOutput :: (Generic a, Generic b) => String -> (a -> b) -> a -> b -> IO ()

equivCheckVisInput :: (Generic b, Generic b1, Generic a) => (a -> b1) -> (a -> b) -> a -> IO ProofResult