Attention une mise à jour du service Gitlab va être effectuée le mardi 14 décembre entre 13h30 et 14h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit b6464fac authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

verifythis_fm2012_treedel: left and right are ghost functions

parent 4d1a93e2
......@@ -66,12 +66,12 @@ module Treedel
forall z "induction": zipper 'a, x: 'a, l r: tree 'a.
inorder (zip (Node l x r) z) = inorder l ++ Cons x (inorder (zip r z))
let left (t: tree pointer) =
let ghost left (t: tree pointer) =
requires { t <> Empty }
ensures { match t with Empty -> false | Node l _ _ -> result = l end }
match t with Empty -> absurd | Node l _ _ -> l end
let right (t: tree pointer) =
let ghost right (t: tree pointer) =
requires { t <> Empty }
ensures { match t with Empty -> false | Node _ _ r -> result = r end }
match t with Empty -> absurd | Node _ _ r -> r end
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment