FStarLang/FStar

Issues

• An interfaced module that references itself wrongly cause a dependency cycle

  #3311 opened 2 days ago by TWal
  0

• Bad type inference when using record disambiguation with monads

  #3310 opened 2 days ago by TWal
  0

• Bad type inference when using subtyping with monads

  #3309 opened 2 days ago by TWal
  0

• Invalid OCaml extracted when using `{ record with update }` syntax for dependent types with exactly one data constructor

  #3258 opened 2 months ago by chandradeepdey
  0

• String length lemma violation in the generate ocaml code !

  #3296 opened 21 days ago by skmuduli92
  3

• Typeclass on eqtype is not resolved when at the end of a type in lax mode (hence dependency loading)

  #3286 opened 12 days ago by TWal
  1

• Incorrect OCaml extraction

  #3307 opened 12 days ago by R1kM
  0

• Extraction loop during `is_arity`

  #3302 opened 17 days ago by mtzguido
  0

• Wish: show implicits by default when they are an override

  #3295 opened 22 days ago by mtzguido
  0

• Bad resugaring of operator when implicits are on

  #3292 opened 23 days ago by mtzguido
  0

• Typeclasses: meta argument of `solve` is sometimes not to instantiated

  #3264 opened a month ago by W95Psp
  1

• Confusing behavior with refinements

  #3282 opened a month ago by mtzguido
  1

• Variable not found with dependent record and pattern matching

  #3266 opened a month ago by nikswamy
  0

• No resugaring of projections

  #3227 opened a month ago by mtzguido
  0

• --cache_dir creates directory, but only one level deep

  #3176 opened a month ago by mtzguido
  1

• Stack overflow with --print_universes

  #3280 opened a month ago by mtzguido
  0

• Fatal error: exception Invalid_argument("output_value: functional value") when I try to print argv to the console.

  #3271 opened a month ago by pantantrant
  1

• `tcresolve`: cannot infer in presence of universe variables

  #3263 opened 2 months ago by W95Psp
  0

• Erasable attribute fails on a type when it shouldn't

  #3252 opened 2 months ago by nikswamy
  0

• Weirdness with tactic failures and --trace_error

  #3249 opened 2 months ago by mtzguido
  0

• Bad(?) performance on long list

  #3246 opened 2 months ago by mtzguido
  0

• Bad typing for range values

  #3238 opened 2 months ago by mtzguido
  0

• Some scoping failures

  #3236 opened 2 months ago by mtzguido
  0

• strict_on_args on recursive function

  #3234 opened 2 months ago by mtzguido
  1

• Qualifiers are sensitive to ordering

  #3232 opened 2 months ago by R1kM
  0

• Limitation when matching pair of indexed types

  #3230 opened 2 months ago by mtzguido
  0

• Stack overflow on Core.check_equiv

  #3224 opened 3 months ago by mtzguido
  0

• Spurious warning on mutually recursive functions

  #3220 opened 3 months ago by nikswamy
  1

• Unifier causing normalization loops (zeta enabled in `equal` heuristic)

  #3207 opened 4 months ago by andricicezar
  4

• Unsoundness due to bad simplification

  #3213 opened 4 months ago by mtzguido
  0

• Preprocess tactic gets "stuck" visiting letrecs sometimes

  #3210 opened 4 months ago by amosr
  2

• Preprocess tactic is not able to reconstruct terms involving records/structs

  #3209 opened 4 months ago by amosr
  0

• Difference in case sensitive for modules and filenames

  #3206 opened 4 months ago by mtzguido
  0

• `&` produces dependent tuples instead of ordinary ones if the constituents are named

  #3198 opened 4 months ago by chandradeepdey
  2

• NBE: eta expansion generates ill-typed terms

  #3185 opened 4 months ago by amosr
  1

• Implicit conversion doesn't work if the refinement is an unnamed function parameter

  #3186 opened 4 months ago by chandradeepdey
  0

• Antiquotations broken badly

  #3192 opened 5 months ago by mtzguido
  0

• Cross-module-inlining behaves inconsistently and differently than friending

  #3188 opened 5 months ago by gebner
  0

• Formatter unfolds unnamed function parameter with refinements weirdly

  #3187 opened 5 months ago by chandradeepdey
  0

• nix: bootstrap is broken

  #3181 opened 6 months ago by pnmadelaine
  1

• fstarlang/fstar-emacs not ready to allow an FStar re

  #3183 opened 6 months ago by briangmilnes
  0

• Failure of tactic in --lax

  #3175 opened 6 months ago by mtzguido
  1

• Squash confusion in calc proofs

  #3173 opened 6 months ago by mtzguido
  0

• Generate all projectors/method via the tactic

  #3166 opened 6 months ago by mtzguido
  2

• Strange error message on missing proof term when you try the syntactic sugar, subtyping? points only to a quantifier variable

  #3153 opened 6 months ago by briangmilnes
  0

• --MLish --lax accepts bad definition

  #3151 opened 6 months ago by mtzguido
  1

• `*` and `&` don't coincide

  #3145 opened 6 months ago by mtzguido
  1

• `let` in decreases clauses crashes F*

  #3140 opened 6 months ago by nikswamy
  0

• cannot be installed via `opam pin` in `opam` sandboxes

  #3144 opened 6 months ago by shonfeder
  1

• Implicits checked twice?

  #3135 opened 6 months ago by mtzguido
  0