-
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
La mise à jour de gitlab est terminée. Nous sommes désormais en version 16.11.1
Merci de consulter la release note:
https://about.gitlab.com/releases/2024/04/18/gitlab-16-11-released/
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