Landon Fuller

This avoids emitting no-op witness/recall calls in the generated code.

``` module Example let example _ = Type u#a -> Type ``` Fails with: `(Error 18) ASSERTION FAILURE: Universe variable U_name a not found`

Verification of the following fails with an internal error: ```fstar module Example open FStar.Seq let compose g f x = g (f x) assume val map (#a #b:Type) (f:a ->...

Given the following test case: ```fstar module Example module B = LowStar.Buffer module HS = FStar.HyperStack module ST = FStar.HyperStack.ST noeq type foo = { ptr:B.pointer_or_null unit } let test...

Unused argument elimination discards required field

1

The following fails with an assert in `krml` (see below) ```fstar module CB = LowStar.ConstBuffer module U8 = FStar.UInt8 module U32 = FStar.UInt32 inline_for_extraction type buftype = | CONST inline_for_extraction...

This adds support for defining a manifest content_script section.

Mixing effects and dependent tuple types

5

Originally ran into this trying to mix the Stack effect with a dependent record type; narrowed the reproduction case down to: ```fstar type pos = (len:nat & (n:nat { n...