[Why3-club] inlining functions or explicit predicates

Jean-Jacques Levy jean-jacques.levy at inria.fr
Tue Feb 19 15:33:11 CET 2019


Dear Jean-Christophe + Friends,

me again (* sorry *) .. a quick view about polymorphic equality: 

Equality in logic should be distinct from Equality in regular code, where the ghost attribute is prohibited. So if the problem with the ghost values is only about aggregated data with ghost components, we could still use ‘Fset’ functions in regular code on non ghost values… Correct ? Is this too simple minded ?

Cheers, -JJ-



More information about the Why3-club mailing list