Is there support for Haskell-like "as-patterns"?

[anton-trunov]

Sorry if I missed this in the docs, but is there support for Haskell-like "as-patterns"? I.e. something like

Equations foo s :=
  foo [] := ...
  foo s@(x :: s') := ... (* s is in scope here *) ...

[Tuplanolla]

While match has such a feature, it does not seem to be recognized by Equations.

Program Fixpoint base_fix (a : N) {measure a lt} : N :=
  match a with
  | N0 => 0
  | Npos _ as n =>
    let p := pred n in
    Npos (stride p) + base_fix p
  end.

Fail Equations base_fix (a : N) : N by wf a lt :=
  base_fix N0 := 0;
  base_fix (Npos _ as n) :=
    let p := pred n in
    Npos (stride p) + base_fix p.

[mattam82]

Yep, that's not supported yet. As the patterns are actual terms this poses a syntax issue, I need to find a way to parse as x as part of terms.