FStar

FStar copied to clipboard

Should `--dep` really emit `.krml` targets for files explicitly excluded by `--extract` ?

5

Currently, when generating a dependency file with `--dep`, F* produces rules for `.krml` files for all modules in the dependency cone of the files provided on the command line argument,...

tahina-pro

The following fails, if we uncomment `assert_spinoff` then it succeeds. The reason is that `pts_to` gets reduced to `Mk_vprop` with lambdas as arguments, that end up getting different smt encoding:...

aseemr

Consider this program: ``` module Repro open Proj assume val t : nat -> Type0 noeq type test = { x:nat; y:t x; } %splice[x_of_test; y_of_test] (mk_projs (`%test) ["x_of_test"; "y_of_test"])...

nikswamy

As @aseemr asked, I'm creating this issue with the following minimal example code: ```fstar assume val f : unit -> Pure int (requires True) (ensures fun x -> x >=...

hacklex

A formula like `forall x1. forall. x2. exists x3. phi` gets resugared to, and hence pretty printed as, `forall x1 x2 x3. phi`. The bug is in the `uncurry` function...

aseemr

``` module Example let example _ = Type u#a -> Type ``` Fails with: `(Error 18) ASSERTION FAILURE: Universe variable U_name a not found`

landonf

Hello! I've done the tutorial, read through the documentation and searched online but couldn't find an explanation on exactly how to do it. I need to have a global state...

hacdias

Verification of the following fails with an internal error: ```fstar module Example open FStar.Seq let compose g f x = g (f x) assume val map (#a #b:Type) (f:a ->...

landonf

@john-ml reports the following failing code: ``` noeq type fn a b = { f: a -> b } let extract_left #a #b : fn (x:either a b{Inl? x}) a...

aseemr

The following definition is rejected: ```fstar let forall_and (p: 'a -> prop) (q: 'b -> prop) (g:(x:'a -> Lemma (p x) [SMTPat (p x)])) (h:(y:'b -> Lemma (q y) [SMTPat...

john-ml