Issues · Why3 / why3 · GitLab

Extend sets with filter and cartesian product

#579 · created Jun 07, 2021 by Quentin Garchery component: theories
- 7
updated Jun 11, 2021
Record transformation time

#574 · created Apr 29, 2021 by Quentin Garchery To be discussed component: session component: transformations feature wish
- 11
updated May 05, 2021
Opening scopes at top level

#573 · created Apr 29, 2021 by Xavier Denis
- 11
updated Apr 30, 2021
Improve the `type mismatch` message

#572 · created Apr 23, 2021 by MARCHE Claude
- 1
updated Apr 23, 2021
CVC4 memlimit registered as high failure

#571 · created Apr 19, 2021 by Johannes Kanig
- 7
updated May 05, 2021
Functions that could be used as let-functions

#570 · created Apr 09, 2021 by Loïc Correnson component: documentation
- 14
updated Apr 16, 2021
Use lemma function like « by » operator

#569 · created Apr 09, 2021 by Loïc Correnson
- 1
updated Apr 09, 2021
unused variables

#568 · created Apr 01, 2021 by Jean-Christophe Filliâtre
- 0
updated Apr 01, 2021
wish: provide monomorphic, clonable modules for references and arrays

#567 · created Mar 31, 2021 by MARCHE Claude 1.5.0 To be discussed component: drivers component: theories component: transformations
- 14
updated May 21, 2021
Whyconf API returns empty config

#564 · created Mar 22, 2021 by Frédéric Blanqui component: configuration
- 4
updated Mar 22, 2021
Extraction of records with a single field

#562 · created Mar 15, 2021 by Benjamin Terra-Jorge 1.4.1 component: extraction
- 0
updated Mar 19, 2021
Vanished invariant "expl" attribute

#559 · created Feb 24, 2021 by Denis Cousineau
- 2
updated Feb 24, 2021
Build a glossary of error messages

#557 · created Feb 23, 2021 by MARCHE Claude component: documentation
- 0
updated Mar 01, 2021
Unused variable

#556 · created Feb 22, 2021 by Guillaume Cluzel
- 1
updated Feb 23, 2021
Add support for `string` type and module `io` in `why3 execute`

#555 · created Feb 19, 2021 by MARCHE Claude 1.5.0 component: execution
- 1
updated Mar 01, 2021
Document the modulo `io`, document printing capabilities

#554 · created Feb 19, 2021 by MARCHE Claude 1.5.0 component: documentation
- 0
updated Mar 01, 2021
RFC: binders for tuple components in function prototype

#552 · created Feb 10, 2021 by Jean-Christophe Filliâtre component: syntax feature wish
- 2
updated Feb 11, 2021
Module `mach.bv` should provide purely bitvector-based pre-conditions

#551 · created Feb 09, 2021 by MARCHE Claude 1.5.0 component: theories
- 1
updated Feb 12, 2021
Syntactic sugar for lemma functions

#547 · created Feb 03, 2021 by Loïc Correnson component: syntax feature wish
- 2
updated Apr 09, 2021
Inductive proofs on inductives

#546 · created Feb 03, 2021 by Loïc Correnson component: core feature wish
- 10
updated Feb 11, 2021

Prev
1
2
3
4
5
…
7
Next