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 27
    • Merge requests 27
  • 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
  • #72
Closed
Open
Issue created Jan 11, 2018 by CLOCHARD Martin@mclochar

Coercion and Higher-Order

Coercions are not applied under implicit higher-order application.

Examples:

module Foo1
  type t
  type u
  function f t : u
  meta coercion function f
  constant g : u -> bool
  goal G : forall x:t. g x
end
module Foo2
  type t
  type u
  function f t : u -> u
  meta coercion function f
  goal G : forall x:t,y:u. x y = y
end

In both modules, the occurrence of "x" within the goal is not coerced as one would expect, leading to a type error. However, when one explicit the higher-order application (operator (@)), those occurrences are coerced as expected.

Edited Jan 11, 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