Search results

normalize_term is unfolded in hovers

Status: Open.

#4311 In FStarLang/FStar;

· gebner opened on Jun 11, 2026

Problems opening a module that was previously imported under a given name

Status: Open.

#4301 In FStarLang/FStar;

· jberthold-ms opened on Jun 7, 2026

Pulse existential inference fails when struct field appears in separation logic predicate

Status: Open.

#4298 In FStarLang/FStar;

· gebner opened on Jun 3, 2026

Ascriptions in local lets seemingly dropped

Status: Open.

#4291 In FStarLang/FStar;

· mtzguido opened on Jun 2, 2026

ANF + ascription does not work

Status: Open.

#4290 In FStarLang/FStar;

· mtzguido opened on Jun 2, 2026

Implement iota-simplification in Pulse contexts

Status: Open.

#4274 In FStarLang/FStar;

· gebner opened on May 22, 2026

Backward errors

Status: Open.

#4267 In FStarLang/FStar;

· mtzguido opened on May 18, 2026

Example of matching loop

Status: Open.

#4264 In FStarLang/FStar;

· mtzguido opened on May 17, 2026

Simple expression if fails

Status: Open.

#4263 In FStarLang/FStar;

· mtzguido opened on May 16, 2026

A val can break a proof

Status: Open.

#4245 In FStarLang/FStar;

· mtzguido opened on May 5, 2026

Semi-unsoundness: all magics are equal, all admits are equal

Status: Open.

#4244 In FStarLang/FStar;

· mtzguido opened on May 5, 2026

@@@strictly_positive cannot be an attribute, or must affect SMT encoding

kind/unsoundnessA bug that has the potential to cause unsoundness, be it ill-typing or proofs of FalseA bug that has the potential to cause unsoundness, be it ill-typing or proofs of False

Status: Open.

#4227 In FStarLang/FStar;

· mtzguido opened on Apr 29, 2026