Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • why3 why3
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 135
    • Issues 135
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 18
    • Merge requests 18
  • Deployments
    • Deployments
    • Releases
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • Why3
  • why3why3
  • Issues

  • Open 6
  • Closed 45
  • All 51
New issue
  • 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