Skip to content

Issues: Beluga-lang/Beluga

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

65 Open 123 Closed
65 Open 123 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

[checkSub] encountered MSVar (checking non-whnf substitution) A | core affecting the typechecker B | bug unexpected or incorrect behaviour
#274 opened Aug 8, 2024 by ryanakca
Internal error: [fmt_ppr_lf_infix_operator] spine length <> 2 A | printing affecting the pretty-printer, error messages, etc. B | bug unexpected or incorrect behaviour
#272 opened Jul 3, 2024 by ryanakca
3
File "src/core/lfrecon.ml", line 1205, characters 9-14: Pattern matching failed A | core affecting the typechecker B | bug unexpected or incorrect behaviour
#269 opened Jun 6, 2023 by ryanakca
Uncaught exception: "missing type information" A | core affecting the typechecker B | bug unexpected or incorrect behaviour
#268 opened Jun 2, 2023 by ryanakca
1
Degraded performance of auto-invert-solve in OCaml 5.0.0 A | proof search affecting the proof search algorithm B | performance correct, but slow
#267 opened May 17, 2023 by MartyO256
1
Harpoon: Uncaught exception when attempting to split/invert something A | core affecting the typechecker A | harpoon affecting the Harpoon interactive prover B | bug unexpected or incorrect behaviour
#257 opened Nov 8, 2022 by chutasano
1
Internal error A | frontend related to the lexer or parser B | enhancement new features
#253 opened Jan 30, 2022 by mb64
1
Dune environment variables suppressing compiler warnings A | misc miscellaneous issues B | refactor changing the implementation of existing features
#244 opened May 25, 2021 by MartyO256
1
some in context schema as requirement for instantiating block A | core affecting the typechecker B | bug unexpected or incorrect behaviour
#242 opened May 14, 2021 by MartyO256
Context schema subsumption A | core affecting the typechecker B | enhancement new features
#241 opened May 14, 2021 by MartyO256
Incorrect totality check for weak normalization example A | core affecting the typechecker A | totality affecting the coverage or wellfoundedness checker B | bug unexpected or incorrect behaviour
#240 opened Apr 29, 2021 by Lysxia
Bug in beluga-mode holes A | interactive-mode affecting the basic interactive mode `beluga -I` B | bug unexpected or incorrect behaviour
#239 opened Mar 31, 2021 by sarahzrf
Added VS Code syntax highlighting for Beluga A | frontend related to the lexer or parser B | enhancement new features
#238 opened Mar 25, 2021 by thesophiaxu
3
Inconsistent behaviour when performing case analysis on appeal to the induction hypothesis in Harpoon A | core affecting the typechecker A | harpoon affecting the Harpoon interactive prover B | bug unexpected or incorrect behaviour
#236 opened Oct 6, 2020 by MartyO256
1
Context variable naming conflict when destructuring block A | core affecting the typechecker B | bug unexpected or incorrect behaviour
#235 opened Oct 6, 2020 by MartyO256
1
Type-checking error in Harpoon in variable case for schemas with higher-order LF types A | core affecting the typechecker A | harpoon affecting the Harpoon interactive prover B | bug unexpected or incorrect behaviour
#234 opened Sep 27, 2020 by MartyO256
Type reconstruction fails in Harpoon in the variable case for context schemas of alternating assumptions A | harpoon affecting the Harpoon interactive prover B | bug unexpected or incorrect behaviour
#233 opened Sep 27, 2020 by MartyO256
Type erasure issue in translated program from Harpoon proof A | core affecting the typechecker A | harpoon affecting the Harpoon interactive prover B | bug unexpected or incorrect behaviour
#231 opened Aug 10, 2020 by MartyO256
1
Termination checking for complete induction A | core affecting the typechecker B | enhancement new features
#227 opened Jul 2, 2020 by MartyO256
1
Can't build on WSL and Request for Docker A | misc miscellaneous issues S | question
#224 opened Jul 1, 2020 by d4hines
3
Inverting twice makes a meta-context variable become in scope A | core affecting the typechecker A | harpoon affecting the Harpoon interactive prover B | bug unexpected or incorrect behaviour
#221 opened Jun 15, 2020 by MartyO256
Unbound variable A | core affecting the typechecker B | bug unexpected or incorrect behaviour P | low low priority issue
#220 opened May 31, 2020 by tsani
1
--stop doesn't really work A | harpoon affecting the Harpoon interactive prover B | bug unexpected or incorrect behaviour B | refactor changing the implementation of existing features P | low low priority issue
#212 opened Apr 7, 2020 by tsani
@tsani
1
Harpoon removes a substitution variable from the scope when splitting on a variable using the substitution A | harpoon affecting the Harpoon interactive prover B | enhancement new features P | low low priority issue
#211 opened Apr 4, 2020 by Ailrun
2
Printed names of meta-context variables for a hole do not match with their defined names A | printing affecting the pretty-printer, error messages, etc. B | bug unexpected or incorrect behaviour P | low low priority issue
#208 opened Mar 31, 2020 by Ailrun
2
ProTip! Follow long discussions with comments:>50.