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 165
    • Issues 165
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 25
    • Merge requests 25
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • Why3Why3
  • why3why3
  • Issues
  • #6
Closed
Open
Issue created Oct 19, 2017 by Guillaume Melquiond@melquionOwner

Error-prone behavior when cloning theories

When cloning a theory, the behavior is to keep axioms as axioms, unless the user explicitly put a with lemma foo clause. This approach is error-prone, as it will cause (possibly inconsistent) facts to never get any proof obligation, due to the user forgetting about them at clone time. I suggest that the default behavior be changed so that any cloned axiom produces a proof obligation, unless the user explicitly put a with axiom foo clause. For the sake of conciseness, there should be a special syntax (e.g. with axiom *) to skip over all the remaining cloned axioms. Another possibility would be to not turn cloned axioms into lemmas if none of their symbols got instantiated at clone time.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking