Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 24
    • Merge requests 24
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #225
Closed
Open
Issue created Dec 28, 2018 by Dan Frumin@dfruminContributor

`is_closed_expr` is stronger than stability under `subst`

I think there is a discrepancy between the substitution and is_closed_expr for heap_lang

According to subst, subst x v' (of_val v) = of_val v. However, is_closed_expr (of_val v) = is_closed_val v (https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/heap_lang/metatheory.v#L22) which is not always true.

That means, IIUC, that there are expressions that are not closed, but which are idempotent under the substitution.

Edited Dec 30, 2018 by Dan Frumin
Assignee
Assign to
Time tracking