# WIP: Make `[#]` produce goal with `<pers>` modality if premise is not persistent

This is my attempt at working towards #186

Currently the `iAssert`

has not been fixed yet, but I would like to see if I am at least going in the right direction.
With the modifications you can now use `iSpecialize`

with on persistent hypothesis to produce a persistent result.
E.g. the following works:

```
Lemma test_specialize `{BiBUpd PROP} (P Q : PROP) :
□ P -∗ □ (P -∗ Q) -∗ □ Q.
Proof.
iIntros "#HP #H".
iSpecialize ("H" with "[#]").
{ iIntros "!>". iAssumption. }
iAssumption.
Qed.
```

The following works as well:

```
Lemma test_specialize_2 `{BiBUpd PROP} (P Q : PROP) :
□ P -∗ □ (□ P -∗ Q) -∗ □ Q.
Proof.
iIntros "#HP #H".
iSpecialize ("H" with "[#]").
{ iIntros "!>". iAssumption. }
iAssumption.
Qed.
```

Edited by Robbert Krebbers