Avoid creating "not not" when splitting goals.
When opening the following code in the IDE, the equality x = 0
is colored in pink in both branches after split_vc
. This is incorrect for the else
branch; it should either be green, or the highlighting should encompass the not
. The issue is that the premise for the else
branch is not (not (x = 0))
(with no location on either not
), which confuses the premise highlighter. This pull request works around the issue by simplifying not-not terms when splitting.
use int.Int
let f (x:int) = if not (x = 0) then absurd else absurd