Skip to content
GitLab

WIP: Add `with M` option to `iModIntro` and use to redefine `iNext` to fix issue #331

Closed Robbert Krebbers requested to merge robbert/issue_331 into master

This allows us to not just specify a matching subterm for iModIntro, but also exactly what modality to introduce. This allows us to redefine iNext so that issue #331 can be closed.

I don't quite like the with syntax, so suggestions for improvement are welcome.

Edited by Ralf Jung