Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Issues
Open
6
Closed
45
All
51
New issue
Recent searches
{{formattedKey}}
{{ title }}
{{ help }}
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
Upcoming
Started
{{title}}
None
Any
{{title}}
None
Any
{{title}}
None
Any
{{name}}
Yes
No
Yes
No
{{title}}
{{title}}
Manual
Priority
Created date
Updated date
Milestone due date
Due date
Popularity
Label priority
Manual
Title
Compute inside an hypothesis
#13
· created
Oct 31, 2017
by
DAILLER Sylvain
component: transformations
CLOSED
1
updated
Jan 05, 2018
Add simpl
#14
· created
Oct 31, 2017
by
DAILLER Sylvain
component: transformations
CLOSED
2
updated
Jan 05, 2018
destruct_alg improvement
#15
· created
Oct 31, 2017
by
DAILLER Sylvain
component: transformations
priority: high
CLOSED
2
updated
Nov 15, 2017
subst should remove declarations
#16
· created
Oct 31, 2017
by
DAILLER Sylvain
component: transformations
priority: medium
CLOSED
4
updated
May 16, 2018
Error in transformation remove
#17
· created
Oct 31, 2017
by
DAILLER Sylvain
component: transformations
CLOSED
2
updated
May 10, 2019
Case should add expl to its new subgoals
#18
· created
Oct 31, 2017
by
DAILLER Sylvain
component: transformations
priority: medium
CLOSED
1
updated
Nov 16, 2017
Apply with x
#19
· created
Oct 31, 2017
by
DAILLER Sylvain
Nov 15, 2017
component: transformations
priority: high
CLOSED
2
updated
Nov 16, 2017
recursive destruct
#20
· created
Oct 31, 2017
by
DAILLER Sylvain
component: transformations
CLOSED
1
updated
Apr 29, 2019
induction_pr with arguments
#22
· created
Oct 31, 2017
by
DAILLER Sylvain
component: transformations
priority: low
CLOSED
1
3
updated
Mar 27, 2019
Add a revert transformation
#23
· created
Oct 31, 2017
by
DAILLER Sylvain
component: transformations
CLOSED
1
updated
Dec 20, 2017
Apply coercions in replace parameters
#24
· created
Nov 07, 2017
by
Raphaël Rieu-Helft
component: transformations
CLOSED
1
1
updated
Dec 09, 2019
Do not require the user to provide the labels in replace parameters
#25
· created
Nov 07, 2017
by
Raphaël Rieu-Helft
component: transformations
CLOSED
1
updated
Nov 10, 2017
typing of transformation argument should not ignore coercion
#34
· created
Nov 16, 2017
by
MARCHE Claude
component: transformations
CLOSED
1
updated
Nov 17, 2017
Incorrect ident parsing in transformations
#71
· created
Jan 08, 2018
by
Raphaël Rieu-Helft
component: transformations
priority: high
CLOSED
3
updated
Feb 02, 2018
first_order_matching may instantiate matching variables using bound variables
#79
· created
Jan 22, 2018
by
CLOCHARD Martin
component: transformations
soundness
CLOSED
4
updated
Feb 02, 2018
Improve handling of premises
#88
· created
Feb 14, 2018
by
Guillaume Melquiond
component: graphical user interface
component: transformations
feature wish
CLOSED
5
updated
Aug 29, 2018
Simplification of array initializer for generated Why3 code
#99
· created
Mar 14, 2018
by
DAILLER Sylvain
component: transformations
CLOSED
1
updated
Jun 18, 2019
eliminate_literal, range types and Eprover driver
#101
· created
Mar 27, 2018
by
Raphaël Rieu-Helft
component: drivers
component: transformations
CLOSED
0
updated
Mar 28, 2018
Problem with infix and val predicate in transformations
#114
· created
May 04, 2018
by
DAILLER Sylvain
component: transformations
CLOSED
2
updated
Jul 18, 2018
subst_all and split_intros_goal_wp do not substitute enough
#115
· created
May 07, 2018
by
DAILLER Sylvain
component: transformations
CLOSED
1
updated
May 23, 2018
Array access in transformations with arguments
#116
· created
May 07, 2018
by
DAILLER Sylvain
component: transformations
CLOSED
1
updated
Jul 18, 2018
simplify_trivial_quantification kills some goals
#120
· created
May 22, 2018
by
Raphaël Rieu-Helft
component: transformations
priority: high
CLOSED
4
updated
May 22, 2018
Transformation `apply` and inductive predicates
#126
· created
Jun 01, 2018
by
Guillaume Melquiond
component: transformations
CLOSED
2
updated
Jun 01, 2018
Transformation `split_vc` and term shapes
#128
· created
Jun 01, 2018
by
Guillaume Melquiond
1.0.0
component: session
component: transformations
priority: blocker
CLOSED
1
0
updated
Jun 13, 2018
transformation ``apply`` should consider ``let`` as a premise
#185
· created
Sep 20, 2018
by
MARCHE Claude
component: transformations
feature wish
CLOSED
4
updated
Oct 29, 2018
Modify split_vc to not use simplify_trivial_quantification
#188
· created
Sep 28, 2018
by
Raphaël Rieu-Helft
1.1.0
component: transformations
CLOSED
1
0
updated
Oct 04, 2018
New split_vc sometimes crashes
#195
· created
Oct 02, 2018
by
Raphaël Rieu-Helft
1.1.0
component: transformations
CLOSED
4
updated
Oct 05, 2018
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
--list-transform should print all transformations
#210
· created
Oct 12, 2018
by
DAILLER Sylvain
component: transformations
CLOSED
0
updated
Nov 13, 2018
Restricting behavior of rewrite_list
#226
· created
Oct 29, 2018
by
DAILLER Sylvain
component: transformations
priority: low
CLOSED
2
updated
Nov 07, 2018
Add a transformation destruct*
#231
· created
Nov 07, 2018
by
DAILLER Sylvain
component: transformations
CLOSED
5
updated
Nov 08, 2018
instantiate should be able to remove the general hypothesis
#232
· created
Nov 07, 2018
by
DAILLER Sylvain
component: transformations
CLOSED
1
updated
Sep 24, 2019
Improve apply
#233
· created
Nov 07, 2018
by
DAILLER Sylvain
component: transformations
0
updated
Nov 07, 2018
Avoid substituting to proxy symbols
#235
· created
Nov 13, 2018
by
DAILLER Sylvain
component: transformations
CLOSED
2
updated
Nov 16, 2018
Improve case transformation
#238
· created
Nov 14, 2018
by
DAILLER Sylvain
component: transformations
CLOSED
1
updated
Jun 18, 2019
improve destruct_alg
#259
· created
Jan 28, 2019
by
MARCHE Claude
component: transformations
CLOSED
1
2
updated
Jan 31, 2019
Removing Inline_trivial
#263
· created
Jan 31, 2019
by
DAILLER Sylvain
component: drivers
component: transformations
CLOSED
1
0
updated
Feb 12, 2019
destruct improvement with if then else
#264
· created
Jan 31, 2019
by
DAILLER Sylvain
component: transformations
CLOSED
2
2
updated
Feb 08, 2019
transformation replace should replace also under the conditions of `if`
#269
· created
Feb 05, 2019
by
MARCHE Claude
1.3.0
component: transformations
CLOSED
4
updated
Feb 12, 2019
induction_ty_arg_lex expected behavior
#280
· created
Mar 01, 2019
by
DAILLER Sylvain
component: transformations
CLOSED
1
0
updated
Mar 26, 2019
split_all_full raises out of memory on float theory
#285
· created
Mar 24, 2019
by
DAILLER Sylvain
component: transformations
0
updated
Mar 22, 2022
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
Incorrect goal location after splitting.
#366
· created
Jul 11, 2019
by
Guillaume Melquiond
component: graphical user interface
component: transformations
CLOSED
1
11
updated
Jul 16, 2019
Trivial goals are not user-friendly
#367
· created
Jul 15, 2019
by
Guillaume Melquiond
component: session
component: transformations
CLOSED
5
updated
Dec 04, 2019
Why3 should not introduce spaces in identifiers
#377
· created
Aug 22, 2019
by
DAILLER Sylvain
component: transformations
CLOSED
1
1
updated
Aug 23, 2019
List transformation with arguments and documentation
#380
· created
Sep 03, 2019
by
DAILLER Sylvain
component: transformations
CLOSED
17
updated
Nov 22, 2019
`apply with` and `rewrite with` should give more details (e.g., quantifier names) when the number of arguments do not match
#399
· created
Oct 25, 2019
by
Guillaume Melquiond
component: transformations
CLOSED
1
2
updated
Oct 28, 2019
Hide does not work
#405
· created
Oct 31, 2019
by
DAILLER Sylvain
component: transformations
CLOSED
1
0
updated
Nov 04, 2019
destruct/case transformations incorrectly handle polymorphic formulas
#525
· created
Jan 14, 2021
by
Quentin Garchery
1.4.0
component: transformations
soundness
CLOSED
1
4
updated
Jul 13, 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
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