Mentions légales du service

Skip to content

support for logic defs + decompile translations bool <-> prop

MARCHE Claude requested to merge update-bddinfer into master

This patch extends the BDD-infer engine:

  • logic functions in annotations are supported when they have a definition. In that case, the definition is simply inlined for inference
  • terms where some transparent translation between bool and prop have been added are now supported. For example, a formula like andb b (x=y) is properly normalized into b /\ (x=y) and not the horrible (andb b (if x=y the True else False)) = True

Merge request reports