Oliver Soeser

icon indicating a website link https://www.oliversoeser.com/ icon indicating an email [email protected]

icon location Edinburgh, Scotland icon location Computer Science and Maths student, University of Edinburgh class of 2027.

Results 4 comments of Oliver Soeser

ispecialize terms of the form P ∗ Q -∗ R

This would be achieved by adding the `IntoWand` instance ```lean instance intoWand_sep_wand (p q : Bool) [BI PROP] (P Q R : PROP) : IntoWand p q iprop(P ∗ Q...

ispecialize terms of the form P ∗ Q -∗ R

I do have plans on extending PR #80 further, though probably not with a complete implementation of specialisation patterns. Most important to me is that the parts of `iapply` dealing...

iApply tactic

Claiming this!

iRevert tactic

Claiming this; I've got a working prototype, though it still needs to be extended to deal with additional subtleties.