Quote does not handle ⊣⊢
The solve_sep_equiv
tactic from bi.tactics
cannot be used to solve goals of the form _ ⊣⊢ _
.
This is due to quote
only accepting goals of the form _ ⊢ _
(see here). Can it be made more general?
The solve_sep_equiv
tactic from bi.tactics
cannot be used to solve goals of the form _ ⊣⊢ _
.
This is due to quote
only accepting goals of the form _ ⊢ _
(see here). Can it be made more general?