pattern match against TSyntax and Bool

Stream: metaprogramming / tactics

[nnarek]

I get weird errors or warnings when I try to pattern match against TSyntax and Bool at the same time

import Lean

open Lean Elab Term Meta

def processTerm (si : Bool) (s_term : TSyntax `term) : TermElabM (TSyntax `term) := do
  match si, s_term with
  | Bool.true, `(0) => `(0)
  | Bool.true, `(1) => `(1)
  | Bool.true, _ => `(2)
  | Bool.false, _ => `(3)

from the code below, we can see that Bool.true is interpreted as a local variable, which is strange

import Lean

open Lean Elab Term Meta

def processTerm (si : Bool) (s_term : TSyntax `term) : TermElabM (TSyntax `term) := do
  match si, s_term with
  | Bool.true, `(0) => `(0)
  | Bool.true, `(1) => `(1)
  | Bool.true, _ => `(2)

I guess this is because match expressions have special handling for TSyntax

[Edward van de Meent]

that's exactly right: Matching on quotations is technically a different syntax from your usual matches. (see also this thread.) Because of this, you can't combine the two of them.