Issues · Why3 / why3 · GitLab

type invariant preservation question

#393 · opened Oct 16, 2019 by DAILLER Sylvain Hackathon component: syntax component: wp
- 9
updated Nov 27, 2019
Location of `variant` clause

#348 · opened Jun 18, 2019 by DAILLER Sylvain component: counterexample component: wp
- CLOSED
- 1
updated Jun 19, 2019
Lost location for function argument

#344 · opened Jun 11, 2019 by DAILLER Sylvain component: wp
- 3
updated Jun 26, 2019
Add `(e at label)` as acceptable ghost code

#307 · opened Apr 19, 2019 by François Bobot component: wp feature wish
- CLOSED
- 6
updated Apr 20, 2019
Add injectivity for type invariant

#287 · opened Mar 26, 2019 by François Bobot component: wp
- 7
updated Oct 25, 2019
Extend witness grammar for type invariant

#286 · opened Mar 26, 2019 by François Bobot component: wp
- 9
updated Mar 26, 2019
Cloning part of mutable structure

#258 · opened Jan 28, 2019 by François Bobot component: theories component: wp
- CLOSED
- 1
updated Jan 28, 2019
Adding location to SP generated variables

#229 · opened Nov 06, 2018 by DAILLER Sylvain component: wp
- 2
updated Nov 07, 2018
Make `any ... ensures` less error-prone

#136 · opened Jun 15, 2018 by Guillaume Melquiond 1.0.0 component: wp
- CLOSED
- 2
updated Jun 22, 2018
Variants and soundness guarantees

#57 · opened Dec 15, 2017 by Guillaume Melquiond component: wp soundness
- CLOSED
- 0
updated Jun 13, 2018
No default order for range types

#56 · opened Dec 14, 2017 by Guillaume Melquiond component: wp
- CLOSED
- 0
updated Sep 14, 2018
Machine integers and range types

#29 · opened Nov 09, 2017 by Guillaume Melquiond 1.0.0 component: theories component: wp
- CLOSED
- 1
updated Feb 02, 2018