Local opens

Similarly to the OCaml let open construct, we have:

let example1 =
let open FStar.List in
rev (append [] [])
 
let example2 =
FStar.List.(rev (append [] []))

The two notations exactly have the same meaning.

Modules or namespaces must be either fully qualified, or be a module abbrev, such as in the following examples, which have exactly the same meaning:

module L = FStar.List
 
let example1 =
  let open L in
  rev (append [] [])
 
let example2 =
  L.(rev (append [] []))

However, you cannot do the following:

open FStar
 
let example3 =
  List.(rev (append [] []))

because List would be treated as the namespace List, not FStar.List as one might think. (In other words, module name M in let open M is rewritten only with module abbrevs, not with namespaces.)

For more details on the latter, and other improvements on namespace resolution (shadowing, etc.) please refer to: Modules, namespaces and name resolution.

NOTE: the Namespace.(term) notation now supersedes the Namespace (term) notation, per pull request #772.