Issues · Why3 / why3 · GitLab

Conversion Float - Signed Bitvectors

#593 · created Oct 06, 2021 by Guillaume Cluzel ProofInUse/TrustInSoft component: theories
- 0
updated Apr 08, 2022
New function for conversion from real to float

#585 · created Jul 22, 2021 by Guillaume Cluzel component: theories
- 1
- 3
updated Sep 22, 2021
Extend sets with filter and cartesian product

#579 · created Jun 07, 2021 by Quentin Garchery component: theories
- 8
updated Jun 27, 2021
wish: provide monomorphic, clonable modules for references and arrays

#567 · created Mar 31, 2021 by MARCHE Claude To be discussed component: drivers component: theories component: transformations
- 14
updated Mar 22, 2022
list functions to move from "function" to "let function"

#504 · created Sep 24, 2020 by Jean-Christophe Filliâtre component: theories
- 0
updated Oct 23, 2020
Simplify bitvector module `Bv`

#500 · created Sep 10, 2020 by Benedikt Becker component: theories
- 0
updated Oct 23, 2020
Module `Cursor` should be documented

#337 · created Jun 05, 2019 by MARCHE Claude component: documentation component: theories
- 0
updated Sep 22, 2021
Add program equality on Boolean type

#306 · created Apr 19, 2019 by MARCHE Claude component: theories
- 2
updated Mar 22, 2022
usage of array.Array should not enforce polymorphic VCs

#193 · created Oct 02, 2018 by MARCHE Claude component: theories
- 0
updated Feb 11, 2021
range types should introduce an injectivity axiom

#97 · created Mar 07, 2018 by MARCHE Claude component: theories
- 9
updated Oct 28, 2020