Issues
- 4
Refinement subtypes being discarded
#3426 opened by amosr - 1
Weirdness with tactic failures and --trace_error
#3249 opened by mtzguido - 0
- 0
warn 331 on useful documentation names in fstar.2024.01.13~dev/ocaml/_build/install/default/bin/fstar
#3372 opened by briangmilnes - 1
- 0
F# extraction rely on unsupported features of F#
#3368 opened by kant2002 - 0
Incorrect erasure of function types
#3366 opened by gebner - 0
Inconsistent subtyping with covariance
#3361 opened by gebner - 1
Normalizer has weird behavior with one-element lists (again)
#3360 opened by TWal - 0
Weird transient issue in steel, gensym collision?
#3358 opened by mtzguido - 2
Normalizer has weird behavior with one-element lists
#3353 opened by TWal - 0
Apparent mismatch between val and let
#3344 opened by mtzguido - 0
Implicits are too eager
#3339 opened by mtzguido - 0
Checked files should be mindful of options
#3333 opened by mtzguido - 0
Add a way to match a constructor with any number of args
#3320 opened by mtzguido - 1
bad error: `Expected type Type0, got type Type0`
#3319 opened by mtzguido - 4
`&` produces dependent tuples instead of ordinary ones if the constituents are named
#3198 opened by chandradeepdey - 0
Resugaring/printing called during normal checking
#3315 opened by mtzguido - 2
Bad type inference when using subtyping with monads
#3309 opened by TWal - 1
- 0
Functions in FStar.List.Pure are not in fstarlib
#3312 opened by TWal - 0
- 0
Invalid OCaml extracted when using `{ record with update }` syntax for dependent types with exactly one data constructor
#3258 opened by chandradeepdey - 3
- 1
Typeclass on eqtype is not resolved when at the end of a type in lax mode (hence dependency loading)
#3286 opened by TWal - 0
Incorrect OCaml extraction
#3307 opened by R1kM - 0
Extraction loop during `is_arity`
#3302 opened by mtzguido - 0
- 0
Bad resugaring of operator when implicits are on
#3292 opened by mtzguido - 1
- 1
Confusing behavior with refinements
#3282 opened by mtzguido - 0
- 0
No resugaring of projections
#3227 opened by mtzguido - 0
Stack overflow with --print_universes
#3280 opened by mtzguido - 1
Fatal error: exception Invalid_argument("output_value: functional value") when I try to print argv to the console.
#3271 opened by pantantrant - 0
`tcresolve`: cannot infer in presence of universe variables
#3263 opened by W95Psp - 0
Erasable attribute fails on a type when it shouldn't
#3252 opened by nikswamy - 0
Bad(?) performance on long list
#3246 opened by mtzguido - 0
Bad typing for range values
#3238 opened by mtzguido - 0
Some scoping failures
#3236 opened by mtzguido - 1
strict_on_args on recursive function
#3234 opened by mtzguido - 0
Qualifiers are sensitive to ordering
#3232 opened by R1kM - 0
Limitation when matching pair of indexed types
#3230 opened by mtzguido - 0
Stack overflow on Core.check_equiv
#3224 opened by mtzguido - 1
Spurious warning on mutually recursive functions
#3220 opened by nikswamy - 4
- 0
Unsoundness due to bad simplification
#3213 opened by mtzguido - 2
Preprocess tactic gets "stuck" visiting letrecs sometimes
#3210 opened by amosr - 0
- 0
Difference in case sensitive for modules and filenames
#3206 opened by mtzguido