Patterns in letbindings

FStarLang / pulse

The Pulse separation logic DSL for F*

Apache License 2.0

6 stars 7 forks source link

Closed mtzguido closed 2 months ago

mtzguido commented 2 months ago

Support patterns in letbindings, like

  let Mktuple2 x y = foo();
  ...

By desugaring into

  let _letpattern = foo();
  match _letpattern {
    Mktuple2 x y -> { ... }
  }

We should also add sugar for tuples and lists in patterns.