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

Giving and solving don't insert parenthesis for applications in dot pattern #3033

Closed
sattlerc opened this issue Apr 16, 2018 · 1 comment
Closed
Assignees
Labels
dot patterns "Forced" (.x) patterns, wirtten by the user or generated by case splitting give Problems with the "give" command interaction-solve type: bug Issues and pull requests about actual bugs ux: interaction Issues to do with interactive development (holes, case splitting, etc)
Milestone

Comments

@sattlerc
Copy link
Contributor

Probably known or duplicate of existing issue. Tested on master.

postulate
  A : Set
  B : Set
  a : A
  f : A  B

data C : B  Set where
  c : C (f a)

foo : (b : B)  C b  Set
foo .{!f a!} c = {!!}

Giving f a in or solving the first hole produces

foo .f a c = {!!}

failing to insert parentheses around the dot pattern.

@sattlerc sattlerc added type: bug Issues and pull requests about actual bugs ux: interaction Issues to do with interactive development (holes, case splitting, etc) give Problems with the "give" command interaction-solve dot patterns "Forced" (.x) patterns, wirtten by the user or generated by case splitting labels Apr 16, 2018
@andreasabel andreasabel self-assigned this Apr 16, 2018
@andreasabel andreasabel added this to the 2.5.4 milestone Apr 16, 2018
@andreasabel
Copy link
Member

Very low hanging fruit, when you know where to look: in ConcreteToAbstract, going inside dot patterns needs to enter DotPatternCtx.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
dot patterns "Forced" (.x) patterns, wirtten by the user or generated by case splitting give Problems with the "give" command interaction-solve type: bug Issues and pull requests about actual bugs ux: interaction Issues to do with interactive development (holes, case splitting, etc)
Projects
None yet
Development

No branches or pull requests

2 participants