iris-lean icon indicating copy to clipboard operation
iris-lean copied to clipboard
verified publisher icon leanprover-community

iApply tactic

Open markusdemedeiros opened this issue 8 months ago • 1 comments

The current tactic suite does not include iApply. It is currently unclear to me how much from MoSEL needs to be ported to implement this, so this issue might make sense to break up into smaller pieces.

markusdemedeiros avatar May 14 '25 20:05 markusdemedeiros

Claiming this!

oliversoeser avatar Jul 07 '25 09:07 oliversoeser