Théophile Wallez
Théophile Wallez
See the following code: ```fstar assume val t1: Type0 assume val t2: t1 -> Type0 type pred (a:Type0) = a -> int -> int -> prop val the_pred: x:t1 ->...
The `CanonCommSemiring` currently doesn't allow semirings to be parametrized with implicit parameters. Allowing this would be very useful, for example to define a ring of integers "modulo m", where `m`...
Look at the file `Heing.fst`: ```fstar module Heing class typeclass (ty:Type0) = { meh: unit; } assume val the_ty: Type0 assume val the_pf: typeclass the_ty instance _: typeclass the_ty =...
See the following example, discussed on Slack a week ago (putting it in an issue for posterity & tracking) ```fstar #set-options "--fuel 0 --ifuel 1" assume val ord: Type0 assume...
In order to have better hygiene in my proofs, I tried to make a few of my functions opaque to SMT, in order to force F* to use their lemmas...
See the following code: InterfaceBug.fsti: ```fstar module InterfaceBug open FStar.List.Tot val length_append: #a:Type -> l1:list a -> l2:list a -> Lemma (length (l1@l2) == length l1 + length l2) ```...
See the following code: ```fstar type strictly_positive_func = [@@@ strictly_positive] _:Type0 -> Type0 [@@expect_failure [3]] noeq type ty1_fail (test: strictly_positive_func) = | C1f: test (ty1_fail test) -> ty1_fail test //...
Typeclass on eqtype is not resolved when at the end of a type in lax mode (hence dependency loading)
See this minimal repro: ```fstar class machin (a:eqtype) = { chose: unit; } noeq type truc (a:eqtype) {|machin a|} = { muche: unit; } instance bidule: machin nat = {...
The problem is described in the comments of the following code: ```fstar // Two monads, with returns and binds assume val m1: Type0 -> Type0 assume val m2: Type0 ->...
Similar to #3309, but using record disambiguation to bamboozle the type inference of F*: ```fstar // Two monads, with returns and binds assume val m1: Type0 -> Type0 assume val...