Skip to content
GitLab
Projects Groups Snippets
  • /
  • 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
    • Graph
    • Compare
  • Issues 166
    • Issues 166
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 26
    • Merge requests 26
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar

La mise à jour du service Gitlab est terminée. Merci aux collègues du service de production de la DSI qui ont réalisé cette opération qui outre les aspects évolution du logiciel nous a permis de faire le nécessaire face à des failles de sécurité.
Les principales releases notes concernant cette montée de version sont disponibles ici :
https://about.gitlab.com/releases/2023/01/22/gitlab-15-8-released/
https://about.gitlab.com/releases/2022/12/22/gitlab-15-7-released/
https://about.gitlab.com/releases/2022/11/22/gitlab-15-6-released/

  • Why3Why3
  • why3why3
  • Issues
  • #330
Closed
Open
Issue created May 29, 2019 by PARREIRA PEREIRA Mário José@mparreirContributor

Use hypotheses when doing compile_match

For the following example:

use list.List

constant l: list int = Cons 42 Nil

goal G : 42 = match l with Nil -> 0 | Cons x _ -> x end

if I want to get a goal of the form 42 = 42, I must do first subst_all and only then compile_match is able to give me 42 = 42.

Would it be possible for compile_match to use hypotheses of the form H: e = e' to further simplify goals of the form match e with e' -> ... end ?

Edited May 29, 2019 by PARREIRA PEREIRA Mário José
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking