FStar

FStar copied to clipboard

Existential quantifications over multiple variables behaves oddly

1

Hi, I just ran into the following issue: discharging by Z3 a proposition consisting of one existential quantification over two variables fails while the same proposition spelled out using two...

W95Psp

For tactics that handle their own errors, i.e. those which call `set_dump_on_failure false`, do not a "Tactic failed" prefix. This includes tcresolve and the pulse checker.

mtzguido

Consider the following example: ```fstar class class_a (t: Type0): Type u#1 = { type_a: Type0; f_a: t -> type_a } class class_b (t: Type0): Type u#1 = { super_a: class_a...

W95Psp

In the presence of universe variables, `tcresolve` doesn't work. Consider the following module: ```fstar module Bug class foo (t: Type0): Type = { u: Type } // or this explicit...

W95Psp

```fst module Test type foo = | Foo : m: int -> n: int{n > m} -> foo let bar (f: foo) : foo = { f with n =...

chandradeepdey

Weirdness with tactic failures and --trace_error

1

```fstar open FStar.Tactics.V2 [@@expect_failure] let _ = assert True by begin fail "fail" end let _ = assert True by begin fail "fail" end ``` This module rightly fails: ```...

mtzguido

I noticed (or remembered... I think we noticed this before) that long list literals take a long time to typecheck. I looked at it and I think the root cause...

mtzguido

strict_on_args on recursive function

1

``` [@@strict_on_arguments [0]] let rec cd (x:nat) : nat = if x = 0 then 0 else 1 + cd (x-1) #push-options "--no_smt" let _ = assert_norm (cd 1 >...

mtzguido

Consider the following code: ```fstar module Test inline_for_extraction noextract val f (x:int) : unit noextract inline_for_extraction let f x = () ``` Attempting to typecheck currently raises the following error...

R1kM

```fstar noeq type task_state : int -> Type u#2 = | Ready : post:int -> task_state post let min (post1:int) (post2:int) (x:task_state post1) (y : task_state post2) : prop =...

mtzguido