Mentions légales du service

Skip to content

Avoid creating "not not" when splitting goals.

Guillaume Melquiond requested to merge split-not into master

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

Merge request reports