Skip to content

simplify telescope-based notations

Ralf Jung requested to merge jung/iris:telescope-notation into master

These type annotations are no longer needed once we have a bidirectionality hint on tele_app.

Requires stdpp!342 (merged) and !763 (merged).

Edited by Ralf Jung

Merge request reports