In pHL, the version of the match tactic that is analogous to if (as opposed to the one analogous to rcondt and rcondf) is not implemented, as contrasted with Hoare logic, where it is.
Also, the islossless tactic gets stuck with match statements, which may be related to the previous issue.
In pHL, the version of the
matchtactic that is analogous toif(as opposed to the one analogous torcondtandrcondf) is not implemented, as contrasted with Hoare logic, where it is.Also, the
islosslesstactic gets stuck withmatchstatements, which may be related to the previous issue.