User attribute used to mark tactics used by continuity.

Tactic to apply continuous.comp when appropriate.

Applying continuous.comp is not always a good idea, so we have some extra logic here to try to avoid bad cases.

• If the function we're trying to prove continuous is actually constant, and that constant is a function application f z, then continuous.comp would produce new goals continuous f, continuous (λ _, z), which is silly. We avoid this by failing if we could apply continuous_const.

• continuous.comp will always succeed on continuous (λ x, f x) and produce new goals continuous (λ x, x), continuous f. We detect this by failing if a new goal can be closed by applying continuous_id.

List of tactics used by continuity internally.

Solve goals of the form continuous f.

Version of continuity for use with auto_param.