Cmd API: functor argument
The used functor is specified as a cmd argument however in many cases the functor could be inferred from the parsing result of the given formula. The argument could hence be only required when it is not clear from the logic.
Another possibility I see would be to give the functor to the parser to allow overlapping syntax or do automated embeddings of e.g. K modalities into CL.