split_if1

Stream: Is there code for X?

[Chase Norman]

There is a definition called split_if1 in tactic.split_ifs. I'm looking for a way to split only the top-level ite expression so this sounds like it would be a tactic to do that. However, even with import tactic or
import tactic.split_ifs, I encounter the error: unknown identifier 'split_if1' or unknown identifier 'split_ifs.split_if1' for the two ways I could think of accessing this. Is this definition meant to be used as a tactic? Is there some way of getting the behavior I am looking for without using the tactic?

[Kevin Buzzard]

Is split_if1 in the tactic.interactive namespace? Those are the tactics you can access in begin end blocks.