• Clément Fumex's avatar
    - some modifications to bv.why/mlw : · 8761602f
    Clément Fumex authored
      + size -> size_bv
      + size_int -> size
      + change two_power_size and max_int definitions
      + add axioms to BVConverter
      + new axiom relating nth and nth_bv
      + some reorganisation
    - update coq realisation
    - modify in consequence the relevant examples and pull the completed ones out of in_progress
    8761602f
queens.mlw 4.97 KB