Commit 2023-07-18 03:33 c1d81a5d
View on Github →feat: remove unnecessary Classical.choice in split_ifs (#5575)
In rare cases, Decidable p is not an instance and split_ifs is still classical. I am not familiar with tactic and not sure if there is an easy method to deal with these cases.