Skip to content
GitLab
Projects Groups Topics 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 revisions
  • Issues 174
    • Issues 174
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 30
    • Merge requests 30
  • 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
  • #127
Closed
Open
Issue created Jun 01, 2018 by Jean-Christophe Filliâtre@filliatrOwner

missing encoding of polymorphism

On the following, a call to a prover requiring polymorphism to be encoded fails:

goal G0: (fun x -> x) 0 = 0

For instance:

> why3 prove -P cvc4 test.mlw
 This type isn't supported:
   'a -> 'a
 smtv2: you must encode type polymorphism
Edited Jun 03, 2018 by Guillaume Melquiond
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking