Wingman.KnownStrategies

Documentation

knownStrategies :: TacticsM ()

known :: String -> TacticsM () -> TacticsM ()

deriveFmap :: TacticsM ()

deriveMappend :: TacticsM ()

We derive mappend by binding the arguments, introducing the constructor, and then calling mappend recursively. At each recursive call, we filter away any binding that isn't in an analogous position.

The recursive call first attempts to use an instace in scope. If that fails, it fals back to trying a theta method from the hypothesis with the correct name.

deriveMempty :: TacticsM ()

We derive mempty by introducing the constructor, and then trying to mempty everywhere. This smaller mempty might come from an instance in scope, or it might come from the hypothesis theta.