All issues

Search results

NBE improvements

Status: Open.

#4432 In FStarLang/FStar;

· nikswamy opened on Aug 13, 2026

Pulse support for let mut in a block without an expected postcondition

Status: Open.

#4430 In FStarLang/FStar;

· nikswamy opened on Aug 13, 2026

Better join inference in Pulse

Status: Open.

#4429 In FStarLang/FStar;

· nikswamy opened on Aug 13, 2026

check-universe: a version of check-world that also builds with the latest Z3 master

Status: Open.

#4428 In FStarLang/FStar;

· nikswamy opened on Aug 13, 2026

Restore check-world with a meaningful set of projects to check

Status: Open.

#4427 In FStarLang/FStar;

· nikswamy opened on Aug 13, 2026

Support for exceptions in Pulse

Status: Open.

#4426 In FStarLang/FStar;

· nikswamy opened on Aug 13, 2026

Bidirectionality for postconditions to get better localized messages

Status: Open.

#4425 In FStarLang/FStar;

· nikswamy opened on Aug 13, 2026

Spec purification fails in function call

Status: Open.

#4423 In FStarLang/FStar;

· mtzguido opened on Aug 12, 2026

Book should mention Unicode alternatives

Status: Open.

#4411 In FStarLang/FStar;

· smheidrich opened on Aug 10, 2026

[karamel] Datatype case with a noextract payload type emits an undefined type name in the header (uncompilable C)

Status: Open.

#4408 In FStarLang/FStar;

· gebner opened on Aug 8, 2026

Pulse: bounded_integers now picks bounded_int_pos for 2 + SZ.v n < pow2 16, adding an unprovable > 0 obligation

Status: Open.

#4407 In FStarLang/FStar;

· gebner opened on Aug 8, 2026

eliminate exists with many binders: huge (and eventually unbounded) SMT cost when the body is a folded predicate application

Status: Open.

#4405 In FStarLang/FStar;

· gebner opened on Aug 8, 2026