FStar

FStar copied to clipboard

Hi, Type ascriptions within patterns on binders seem to have no effect. For instance, `f` and `g` below have a pattern as their first binder, pattern which is ascribe the...

W95Psp

This caused the IDE server to crash on some files in pulse.

gebner

Add forall versions of memP_map_intro and memP_map_elim

4

chandradeepdey

- Mirrors TSet - Remove the refinement on the return type of filter, it was implied by the SMTPat on mem_filter_forall anyway

chandradeepdey

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

4

Hi, I have a use case when normalization loops.  Using F* version: 2024.01.13 Sorry for the big file. I removed as many things as I had time. The problem...

andricicezar

Add `[@@no_inline_let]` annotation

9

This adds a `[@@no_inline_let]` annotation so that the norm tactic doesn't always unfold local lets. I had to update the rlimit in some places. Some of these were necessary to...

amosr

Hi, I just noticed that `preprocess_with` does not deal well with records. A record constructor `{ x = 0; y = 1}` generates a term like `__dummy__ 0 1`. If...

amosr

Splitting tuple types into separate modules for each

4

Discussed with @nikswamy today: always loading the definitions for all tuples (normal ones up to 14, dependent up to 5) is an unnecessary load on the typechecker and SMT solver....

mtzguido

``` $ cat AA.fst module Aa ``` ``` $ cat BB.fst module BB open AA ``` Trying to check `BB` gives: ``` $ ./bin/fstar.exe BB.fst * Warning 241 at AA.fst(0,0-0,0):...

mtzguido

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

2

```fstar let this_is_a_pair (a: nat) (b: nat) : nat * nat = a, b let this_is_a_pair' (a: nat) (b: nat) : a': nat * b': nat = a, b let...

chandradeepdey