Gabriel Ebner
Gabriel Ebner
This allows F* to build with OCaml 5.2.0. Fixes #3048
This pushes the CI base image to the `ghcr.io` container registry instead of storing it locally on the build machine. The container registry is publicly accessible, so `make docker-ci` works...
This PR changes the parser to require fewer parentheses: 1. When using lambdas as last function argument: `foo fun x -> x + 1` 2. Around `assume` and `assert` arguments:...
(Following up on the discussion we just had.) F* treats function types with an erasable codomain as erasable themselves. For example, `Type -> Type` is erasable. If such a function...
This is an MWE extracted from the issue I had in the thunk module I showed yesterday. There are three types here, `r` is a subtype of `s`, which is...
Right now we have two separate sets of functions which decide whether a type is erasable/noninformative, one which only looks at `erasable` and another which also looks at `must_erase_for_extraction`. This...
```fstar module Div2 let rec uhoh t : Div t (requires True) (ensures fun _ -> False) = uhoh t let foo (x: option nat) : Dv string = uhoh...
The reflection API only exposes a portion of the syntax AST. Since `FStar.Reflection.Typing.subst_term` is written as a syntax traversal using this limited API, it will silently drop various flags when...
While Z3 4.8.5 builds on aarch64 linux, it segfaults already on the VCs from prims.fst: ``` CHECK prims.fst Unexpected error; please file a bug report, ideally with a minimized version...
Currently all erasable terms are erased to unit. This changes the `non_informative` function to return an `option term` instead of `bool`. This optional term specifies what the type should be...