-
Martin Clochard authored
The following could be proved correct: type t = A | B function f (x:'a) : 'a = x predicate top = A = f A lemma bad : forall x:t. match x with A -> x = B | B -> x = B -> top end lemma fail : false
071a1394
The following could be proved correct: type t = A | B function f (x:'a) : 'a = x predicate top = A = f A lemma bad : forall x:t. match x with A -> x = B | B -> x = B -> top end lemma fail : false