$
Lib.$ : ('a -> 'b) * 'a -> 'b
Right-associated infix function application operator
Writing f $ x is another way of writing f x.
Failure
Fails if f x would fail.
Comments
Because $ is right-associated, this can be a convenient way to avoid
parentheses. For example,
first_x_assum $ qspec_then ‘m’ $ qx_choose_then ‘z’ strip_assume_tac
instead of
first_x_assum (qspec_then ‘m’ (qx_choose_then ‘z’ strip_assume_tac))
Note also that $ is tighter than the various THEN infixes, so a
tactic such as the one above can be used in a proof without needing
protection by extra parentheses.