FStar

FStar copied to clipboard

The query `length l == 10` does not work via SMT due to lack of fuel. So we can attempt to use meta-args to solve the squash via normalization, which...

mtzguido

Eager or lazy instantiation of implicits?

3

Trying to use typeclasses a little... here is my minimal repro: ``` class block (index: Type0) = { // Astract footprint. state: index -> Type0; footprint: #i:index -> h:HS.mem ->...

msprotz

No idea why this is happening, but making a note to not forget ```fstar module XX let x = 1 + 'a' ``` ``` $ ./bin/fstar.exe XX.fst --trace_error Unexpected error...

mtzguido

This snippet leaks a `U_name` in the checked file, apparently since the val is universe-polymorphic, but the let is not. ```fstar module U #set-options "--lax" assume val f : t:Type...

mtzguido

Creating an effect while providing universe level variables produces unexpected error

2

I have an effect where parameters are also universe polymorphic, and since F* requires me to have only one universe variable, I have to set two of them to be...

TheoWinterhalter

This fixes #2933 by adding a `Type` ascription whenever none is present. This does lead to some regressions, since if there was no ascription / expected type we would take...

mtzguido

Crash on lambda

2

```fstar let fix_1 (#a : Type) (#r : (xa:a -> Type)) (#sz : Type) (m : a -> sz) (ff : (x1:a -> (y1:a{m y1 Tot (r y1)) -> Tot...

mtzguido

Interleaving misses (and therefore keeps) pragmas at the tail of the file

1

Yet another reason to remove interleaving. A.fsti: ```fstar module A #push-options "--z3rlimit 40 --admit_smt_queries true" val lem (x:int) : Lemma True #pop-options ``` A.fst: ```fstar module A let lem (x:int)...

mtzguido

Karamel extraction errors on `noextract` recursive tactic

3

I came across an error when defining a tactic that uses a local recursive definition as well as repeat. The `--codegen krml` extraction fails with a "this should not happen"...

amosr

This is a spinoff of #2986 without actually changing the behavior for typeclass, but with the fixes to make `strict_on_args` definition not unfold unless they are actually applied (currently F*...

mtzguido