Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

crefine: change misleading proof step in CSpace_RAB_C #669

Merged
merged 1 commit into from
Sep 14, 2023
Merged

crefine: change misleading proof step in CSpace_RAB_C #669

merged 1 commit into from
Sep 14, 2023

Commits on Sep 14, 2023

  1. crefine: change misleading proof step in CSpace_RAB_C 

    Trying to figure this out was very educational, since ccorres_abstract
was used without intending to abstract a variable, the xf' and lambda
name were both red herrings (in fact, this proof only worked if xf' was
instantiated with an *irrelevant* C local var name), and the body was
not transformed.

Signed-off-by: Rafal Kolanski <[email protected]>
    @Xaphiosis
    Xaphiosis committed Sep 14, 2023
    Configuration menu
    Copy the full SHA
    3eee267 View commit details
    Browse the repository at this point in the history