Théophile Wallez

See these examples: ```fstar open FStar.All open FStar.Tactics let f (): ML bool = true let fstar_all_ml_name: name = explode_qn "FStar.All.ML" // Destructing a ML comp cause problems [@@expect_failure] let...

See the following example: ```fstar module Test open FStar.Tactics val make_extraction_fail: unit -> Tac nat let make_extraction_fail () = let rec f (n:nat): Tac nat = if n = 0...

See the following code: ```fstar module UnitExtraction let byte = n:nat{n < 256} let lbytes (n:nat) = l:list byte{List.Tot.length l == n} // In my real case, everything is well-encapsulated...

Typeclass resolution don't work with typeclass that depend on others

2

See the following example: ```fstar class tc1 (a:Type) = { tc1_method: unit; } class tc2 (a:Type) {|tc1 a|} (b:Type)= { //This function use the methods of tc1 to do its...

Type inference works in "normal mode" but fails in lax mode (hence in dependency loading)

3

See the following example A.fst: ```fstar module A assume val bytes_like: Type0 -> Type0 assume val parser_serializer: bytes:Type0 -> pf:bytes_like bytes -> Type0 -> Type0 assume val bind: #bytes:Type0 ->...

See the following example, happening in a context similar to #2478 . ```fstar assume val bytes_like: Type0 -> Type0 assume val parser_serializer: Type0 -> Type0 type key (bytes:Type0) (pf:bytes_like bytes)...

`unfold` don't work as expected in binder attributes

1

See the following example: ```fstar module UnfoldAttr open FStar.Tactics irreducible let attrib (#a:Type) (x:a) = () unfold let string_attrib (s:string) = attrib ("[" ^ s ^ "]") type test =...

See the code below: ```fstar let test_annot (#a:Type0) (x:int) = () type test_type = { [@@@ test_annot 1337] x: int; } ``` It gives the following error: ``` ASSERTION FAILURE:...

Proofs made using `unshelve` are forgotten afterward

1

See the following minimal example ```fstar open FStar.Tactics assume val predicate: int -> Type0 // If we add the SMTPat, then `test` succeed assume val predicate_is_true_lemma: x:int -> Lemma (predicate...

`l_to_r` fails when there is subtyping?

1

`l_to_r` do not work in this case: ```fstar open FStar.Tactics assume val length_cons: #a:Type -> x:a -> l:list a -> Lemma (List.Tot.Base.length (x::l) == (List.Tot.Base.length l) + 1) [@@ expect_failure]...