-- Andrei Paskevich (2018-07-25) > This is also on purpose: the tt'int operation is used for > specification purposes, if you make it non-ghost, you would need to > link the extracted code with an arbitrary-precision arithmetic > library.
so type "int" is also ghost? we might need to mark all the generated Why3 code as ghost then. -- Yannick Moy, Senior Software Engineer, AdaCore
_______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
