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

Attention une mise à jour du service Gitlab va être effectuée le mardi 07 février entre 13h30 et 14h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes (habituellement de l'ordre de trois minutes).

  • Why3Why3
  • why3why3
  • Issues
  • #231
Closed
Open
Issue created Nov 07, 2018 by DAILLER Sylvain@sdaillerDeveloper

Add a transformation destruct*

Add a transformation that performs destruct recursively on an hypothesis. It should handle all currently handled constructs: disjunction, conjunction, implications.

predicate p1
predicate p2
predicate p3

axiom H: p1 -> p2 -> p3
goal G: 1 = 1

destruct H should produce 3 new goals for p1, p2 and H : p3 |- G ? [EDIT: To be more clear]

This should produce 3 new subgoals which are the following:

  predicate p1
  predicate p2
  predicate p3
  
  goal G : p1
  predicate p1
  predicate p2
  predicate p3
  
  goal G : p2
  predicate p1
  predicate p2
  predicate p3
  
  axiom H : p3
  goal G : 1 = 1

Sorry for the misleading notations.

Edited Nov 07, 2018 by DAILLER Sylvain
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking