Issues · Why3 / why3 · GitLab

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
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
Bogomips

#494 · created Jul 16, 2020 by Guillaume Melquiond component: tools feature wish
- 0
updated Feb 11, 2021
turn lemma into lemma function automatically

#493 · created Jul 02, 2020 by Jean-Christophe Filliâtre component: syntax feature wish
- 1
- 1
- 16
updated Feb 11, 2021
Syntax `(fun x -> ...)` should always denote a lambda-expression, not a program

#440 · created Feb 05, 2020 by MARCHE Claude 1.5.0 To be discussed feature wish
- 18
updated Jan 22, 2021
Warn about spurious `rec` keyword

#439 · created Feb 04, 2020 by MARCHE Claude 1.5.0 To be discussed feature wish
- 0
updated Jan 22, 2021
Local config file common to all Why3 commands

#430 · created Jan 10, 2020 by MARCHE Claude 1.5.0 To be discussed component: configuration component: tools feature wish
- 1
- 6
updated Feb 15, 2021
Localisation of errors during extraction of cloned module

#403 · created Oct 31, 2019 by DAILLER Sylvain component: extraction feature wish
- 0
updated Oct 31, 2019
Warning on useless exception catching

#394 · created Oct 16, 2019 by DAILLER Sylvain To be discussed feature wish
- 1
updated Nov 08, 2019
Why3 shell improvements 4 of 8 tasks completed

#333 · created Jun 05, 2019 by François Bobot To be discussed component: session server feature wish
- 4
updated Jun 07, 2019
Use hypotheses when doing compile_match

#330 · created May 29, 2019 by PARREIRA PEREIRA Mário José component: transformations feature wish
- 5
updated Oct 28, 2020
Warn about trivially spurious conter-example

#256 · created Jan 28, 2019 by François Bobot component: counterexample feature wish
- 5
updated Jan 07, 2020
Allow "use ghost Foo"

#246 · created Nov 30, 2018 by Guillaume Melquiond To be discussed component: core component: extraction component: syntax feature wish
- 0
updated May 21, 2019
Interaction of smt encoding with meta

#196 · created Oct 03, 2018 by DAILLER Sylvain component: transformations feature wish priority: low
- 3
updated Mar 12, 2021
Miscellaneous feature wishes for discussion

#176 · created Aug 29, 2018 by Benedikt Becker feature wish
- 10
updated Aug 31, 2018
Extraction of absurd

#171 · created Aug 29, 2018 by MARCHE Claude Hackathon component: extraction feature wish
- 4
updated Oct 23, 2020
Commands request to be reorganized

#63 · created Dec 19, 2017 by DAILLER Sylvain component: graphical user interface feature wish
- 1
updated May 30, 2018
additional manually-written configuration files

#55 · created Dec 14, 2017 by CLOCHARD Martin component: configuration feature wish
- 6
updated Feb 15, 2021
Tab completion in the command line

#39 · created Nov 17, 2017 by Raphaël Rieu-Helft component: graphical user interface feature wish
- 1
updated Jun 18, 2019