Skip to content

Renaming inside of clone is very brittle #295

@dorchard

Description

@dorchard

At the moment clone seems to only handle single ids and this also seems brittle as witnessed by the failing tests in example/uniqueness.gr and for example that the following fails:

unitR : forall {a : Type, id : Name} . !(*(Ref id a)) -> exists {id1 : Name} . !(Ref id1 a)
unitR t = clone t as x in share x

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions