Skip to content

Issues: JetBrains/intellij-arend

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

37 Open 312 Closed
37 Open 312 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Incorrect data is fed into DataValidator bug
#528 opened Jul 3, 2024 by sxhya
@sxhya
Support 2024.2 (EAP right now)?
#519 opened Jun 18, 2024 by ice1000
Completion does not work after a dot in meta expressions completion
#461 opened Feb 29, 2024 by valis
@valis
Shift+Ctrl+P should actually typecheck pieces of code upon which it is invoked D-medium feature type checking usability-problem Usability Problem
#430 opened Nov 10, 2023 by sxhya
@alex999990009
Issues with ChangeSignatureRefactoring bug D-hard feature refactoring
#429 opened Nov 6, 2023 by sxhya
1 of 4 tasks
@sxhya
ChangeArgumentExplicitness should work for parameters with \Pi or \Sigma types feature refactoring
#428 opened Nov 6, 2023 by sxhya
@sxhya
Implement Ctrl+Shift+P for patterns D-medium feature
#405 opened Jul 20, 2023 by sxhya
@sxhya
1
Add support of numerals to Arend proof search feature proof-search Arend Proof Search feature
#390 opened Mar 21, 2023 by sxhya
@alex999990009
Warning when attempting to patternmatch on unimported constructors D-medium feature
#388 opened Mar 6, 2023 by sxhya
@alex999990009
Don't use generated PSI in plugin D-hard internal
#378 opened Jul 12, 2022 by knisht
3
Intention/inspection about eta-convertible expressions feature intention
#357 opened Feb 8, 2022 by knisht
Consider adding a completion for unicode symbols in aliases completion feature
#356 opened Feb 8, 2022 by marat-rkh
5
Consider showing math symbols instead of some language constructions D-medium editor feature
#344 opened Dec 6, 2021 by marat-rkh
1
"Split atomic pattern" for let expressions D-medium feature
#308 opened Sep 16, 2021 by marat-rkh
@sxhya
2
"Split atomic pattern" for lambda parameters D-medium feature
#307 opened Sep 16, 2021 by marat-rkh
@sxhya
New inspection: redundant explicit argument feature intention
#294 opened Aug 28, 2021 by marat-rkh
Bug: removing import doesn't lead to error bug type checking
#293 opened Aug 25, 2021 by marat-rkh
@sxhya
Show less errors for code with syntax errors usability-problem Usability Problem
#287 opened Aug 15, 2021 by marat-rkh
False positive "X is not a reference to either a definition or a variable"
#271 opened May 15, 2021 by marat-rkh
@alex999990009
1
Consider showing a type hint for function clauses
#264 opened Apr 20, 2021 by marat-rkh
4
"Fill goal" works incorrectly in presence of ==<, >== and `qed
#263 opened Apr 19, 2021 by marat-rkh
4
Confusing error message about language version on IDE startup
#256 opened Mar 21, 2021 by marat-rkh
2
Intention to generate pattern matching clauses
#253 opened Mar 19, 2021 by marat-rkh
Equational reasoning style support in formatter formatter
#224 opened Aug 10, 2020 by tonyxty
3
Support pure expression highlighting highlighting repl
#210 opened Jul 11, 2020 by ice1000
ProTip! Adding no:label will show everything without a label.