Skip to content

v0.9.6.0-alpha1 (EPIT and SSFT)
Compare
Choose a tag to compare
@danelahman danelahman released this 04 May 08:52
· 20715 commits to master since this release
v0.9.6.0-alpha1
0657452

A preview for an upcoming major release in preparation for several courses and tutorials.

This brings lots of improvements:

  • two-phase type checking (towards disentangling type checking from checking of verification conditions), more robust wrt. inference of implicit arguments
  • extraction to OCaml preserves the structure of let-bindings
  • extraction now erases all pure unit functions, lemmas and ghost functions
  • and many many more, see https://github.com/FStarLang/FStar/blob/v0.9.6.0-alpha1/CHANGES.md for more details.
Assets 5
Loading