FStar
FStar copied to clipboard
FStarLang
A Proof-oriented Programming Language
This PR adds a new variant of the Steel `for_loop` combinator called `for_loop_full`, which supports the additional use of a selector invariant on top of the current vprop invariant. Note,...
This PR adds a new function, called `malloca_of_list` to Steel. Similarly to what was done in Low*, this function takes a list literal, and allocates a new array statically initialized...
This PR adds explicit [permissions section](https://docs.github.com/en/actions/using-workflows/workflow-syntax-for-github-actions#permissions) to workflows. This is a security best practice because by default workflows run with [extended set of permissions](https://docs.github.com/en/actions/security-guides/automatic-token-authentication#permissions-for-the-github_token) (except from `on: pull_request` [from external...
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 ->...
Since this is an important discussion I'm splitting off a separate thread (previous one is https://github.com/FStarLang/FStar/issues/355#issuecomment-139806214). It is folklore in the type theory world that mixing the following, very useful...
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`...
@jaylorch reports that the trefl fails in this program ``` module Test58 let f1 (x: option int) : int = match x with | None -> 0 | Some u...
Hi, As discussed last Monday, this PR, subsequent of #2666, changes the lexer so that the sequence `//` is forbidden in operators. The string `++//*` used to be lexed as...
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 =...
With `ppxlib.0.27.0`, `fstar.2022.08.10~dev` compilation fails with the following error: ``` #=== ERROR while compiling fstar.2022.08.10~dev ===============================# # context 2.1.0 | macos/x86_64 | ocaml-base-compiler.4.12.0 | pinned(git+ssh://[email protected]/FStarLang/FStar.git#c625bb4f) # path ~/.opam/4.12.0/.opam-switch/build/fstar.2022.08.10~dev # command...
