Local opens

Jump to bottom Edit New page

Jonathan Protzenko edited this page Sep 28, 2016 · 6 revisions

Similarly to the OCaml let open construct, we have:

module L = FStar.List

let example1 =
  let open L in
  rev (append [] [])

let example2 =
  L (rev (append [] []))

the latter is slightly different from the OCaml syntax, which would be: L.(rev (append [] [])).