Skip to content

Rename `f_contractive_core` into `dist_later_intro`.

Robbert Krebbers requested to merge robbert/dist_later_intro into master

This MR is based on !886 (merged), so that one needs to be merged first.

In actris!29 (merged) I realized that it is sometimes necessary to apply a Contractive instance yourself. After that, you have a goal of the form dist_later. The tactic f_contractive_core is very useful to introduce such goals, but it currently appears to be intended as an implementation detail. This MR:

  • Renames f_contractive_core into dist_later_intro so that it becomes a proper tactic that downstream users could use.
  • Removes the try from its definition so that it only succeeds if the goal is actually a dist_later. The try has been moved to f_contractive.
  • Provides versions dist_later_intro as n Hn and dist_later_intro without arguments, following the same syntax as f_contractive.
  • Does the same for f_contractive_fin_core.
  • Tweaks the documentation accordingly.

Merge request reports