Pin a variable name in pattern matching

Stream: new members

[Sébastien Boisgérault]

Hello everyone! :wave:

Is there a way to "pin" a variable name in pattern matching? (in Elixir terminology)

I'd like both code snippets below to behave the same way:

#eval match 100 with
  | Nat.succ 6 => true
  | _ => false
-- false

def six := 6

#eval match 100 with
  | Nat.succ six => true -- six is captured, this is not what I want
  |_ => false
-- true

[Henrik Böving]

@[match_pattern]
def six := 6

is what you want

[Robin Arnez]

Note that that only works with definitions and not with variables from the local scope though

[Robin Arnez]

Interestingly enough, matching on local variables is possible but this functionality isn't exposed by the match syntax:

import Lean
import Qq

open Lean Meta Match Qq in

def matchOn (var : Q(Nat)) : MetaM Expr := do
  let matcher ← mkMatcher {
    matcherName := `abc.match_1
    matchType := q(Nat → Unit)
    discrInfos := #[{}]
    lhss := [
      {
        ref := .missing
        fvarDecls := [],
        patterns := [.ctor ``Nat.succ [] [] [.val var]]
      },
      ← withLocalDeclDQ `x q(Nat) fun var =>
        return {
          ref := .missing,
          fvarDecls := [← var.fvarId!.getDecl]
          patterns := [.var var.fvarId!]
        }
    ]
  }
  matcher.addMatcher
  return matcher.matcher

open Qq in

elab:max "my_match " x:term:arg : term => do
  let e ← elabTermEnsuringTypeQ x q(Nat)
  matchOn e

def six := 6

#eval my_match 6 (fun _ => Bool) 100 (fun _ => true) (fun _ => false)
#eval my_match six (fun _ => Bool) 100 (fun _ => true) (fun _ => false)
#eval have six := 6; my_match six (fun _ => Bool) 100 (fun _ => true) (fun _ => false)

def test (x : Nat) :=
  my_match x (fun _ => Bool) 100 (fun _ => true) (fun _ => false)

[Aaron Liu]

it performs a deceq check