Skip to content
GitLab

Better proof mode support for telescope + add missing BI instances

Merged Robbert Krebbers requested to merge robbert/tele into master

This MR adds:

  • Affine, absorbing, persistent and timeless instances for telescopes.
  • Better support for telescopes in the proof mode, i.e., all tactics should recognize and distribute telescopes now.
  • Many test cases to exercise this.