Skip to content

Issues: FStarLang/FStar

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

442 Open 1,535 Closed
442 Open 1,535 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
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

Confusing behavior with refinements
#3282 opened May 2, 2024 by mtzguido
Typeclasses: meta argument of solve is sometimes not to instantiated
#3264 opened Apr 24, 2024 by W95Psp
tcresolve: cannot infer in presence of universe variables
#3263 opened Apr 24, 2024 by W95Psp
Invalid OCaml extracted when using { record with update } syntax for inductive types with exactly one data constructor
#3258 opened Apr 20, 2024 by chandradeepdey
Weirdness with tactic failures and --trace_error
#3249 opened Apr 16, 2024 by mtzguido
Bad(?) performance on long list
#3246 opened Apr 14, 2024 by mtzguido
strict_on_args on recursive function
#3234 opened Apr 7, 2024 by mtzguido
1
Qualifiers are sensitive to ordering
#3232 opened Apr 4, 2024 by R1kM
Limitation when matching pair of indexed types
#3230 opened Mar 28, 2024 by mtzguido
Spurious warning on mutually recursive functions
#3220 opened Mar 3, 2024 by nikswamy
1
Preprocess tactic is not able to reconstruct terms involving records/structs
#3209 opened Feb 9, 2024 by amosr
Unifier causing normalization loops (zeta enabled in equal heuristic)
#3207 opened Feb 8, 2024 by andricicezar
4
Difference in case sensitive for modules and filenames
#3206 opened Feb 6, 2024 by mtzguido
& produces dependent tuples instead of ordinary ones if the constituents are named
#3198 opened Jan 29, 2024 by chandradeepdey
2
Antiquotations broken badly
#3192 opened Jan 18, 2024 by mtzguido
@mtzguido
Cross-module-inlining behaves inconsistently and differently than friending
#3188 opened Jan 10, 2024 by gebner
Formatter unfolds unnamed function parameter with refinements weirdly
#3187 opened Jan 4, 2024 by chandradeepdey
fstarlang/fstar-emacs not ready to allow an FStar re
#3183 opened Dec 23, 2023 by briangmilnes
nix: bootstrap is broken
#3181 opened Dec 22, 2023 by pnmadelaine
1
Failure of tactic in --lax
#3175 opened Dec 19, 2023 by mtzguido
@mtzguido
1
Squash confusion in calc proofs
#3173 opened Dec 19, 2023 by mtzguido
Generate all projectors/method via the tactic
#3166 opened Dec 15, 2023 by mtzguido
@mtzguido
2
* and & don't coincide component/printer
#3145 opened Dec 8, 2023 by mtzguido
1
cannot be installed via opam pin in opam sandboxes
#3144 opened Dec 8, 2023 by shonfeder
1
Implicits checked twice? component/tactics
#3135 opened Dec 6, 2023 by mtzguido
@mtzguido
ProTip! Adding no:label will show everything without a label.