[Why3-club] Realized theories and "remove prop" declarations

Stefan Berghofer berghofe at in.tum.de
Wed Nov 6 15:28:27 CET 2013


Dear Why3-Club,

the file coq-common.gen contains many "remove prop" declarations for theories that are
realized, such as "remove prop Div_mod" for theory int.ComputerDivision. What is the
rationale behind these declarations? Shouldn't a proof obligation be generated to make
sure that the Coq functions ZOdiv and Z0mod behave the same way as the corresponding Why3
functions div and mod?

Greetings,
Stefan



More information about the Why3-club mailing list