Issues · Why3 / why3 · GitLab

More options for `why3 replay` 0 of 3 tasks completed

#651 · created May 24, 2022 by MARCHE Claude component: tools feature wish
- 5
updated May 24, 2022
Misleading "unbound function" error message

#591 · created Sep 27, 2021 by Xavier Denis component: core feature wish
- 1
- 5
updated Sep 27, 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
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
Syntax `(fun x -> ...)` should always denote a lambda-expression, not a program

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

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

#430 · created Jan 10, 2020 by MARCHE Claude To be discussed component: configuration component: tools feature wish
- 1
- 6
updated Mar 22, 2022
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
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
additional manually-written configuration files

#55 · created Dec 14, 2017 by CLOCHARD Martin component: configuration feature wish
- 6
updated Feb 15, 2021