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.

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

"Not a variable error" #2517

Closed
xekoukou opened this issue Mar 27, 2017 · 2 comments
Closed

"Not a variable error" #2517

xekoukou opened this issue Mar 27, 2017 · 2 comments
Assignees
Labels
parameter-refinement regression on master Unreleased regression in development version (Change to "regression in ..." should it be released!) ux: case splitting Issues relating to the case split ("C-c C-c") command
Milestone

Comments

@xekoukou
Copy link

Possibly related to #2183 #2181
When I try to case split on rll :
findCallGraph {ll = ll} {rll = rll} {olf = olf} (call x) if msr ms = {!!}

I get this:

/mnt/Workspace/sparrow/agda/IndexLF.agda:306,70-74
Not a variable: rll
when checking that the expression ? has type
MSetLFCRem olf (call .∞rll) × MSetLFC olf olf

This works fine :

findCallGraph {ll = ll} {rll = call .∞rll} {olf = olf} (call {∞rll = ∞rll} x) if msr ms = {!!} 

Commit to reproduce error:
https://github.com/xekoukou/sparrow/blob/74de191538e421fd0a62f67344c5e83fd18f7612/agda/IndexLF.agda#L306

The error message should be improved. Certainly rll is a variable.

@andreasabel andreasabel added ux: case splitting Issues relating to the case split ("C-c C-c") command parameter-refinement regression on master Unreleased regression in development version (Change to "regression in ..." should it be released!) labels Mar 27, 2017
@andreasabel andreasabel added this to the 2.5.3 milestone Mar 27, 2017
@andreasabel
Copy link
Member

Confirmed that is is #2183.
For now, I am just improving the error message.

@andreasabel
Copy link
Member

Closing, as this is a duplicate of #2183.

@andreasabel andreasabel self-assigned this Mar 31, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
parameter-refinement regression on master Unreleased regression in development version (Change to "regression in ..." should it be released!) ux: case splitting Issues relating to the case split ("C-c C-c") command
Projects
None yet
Development

No branches or pull requests

2 participants