Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: syntax quotation and matching


Edward van de Meent (Apr 02 2025 at 07:35):

in a study group the following question came up:
we can match on syntax using syntax quotations without issue. However, when trying to #check the syntax quotation, we couldn't figure out how to get it to actually be of type Syntax.
modifying an example from the metaprogramming book:

open Lean

def isAdd : Syntax  Option (Syntax × Syntax)
  | `(Nat.add $x $y) => some (x, y) -- works, `(Nat.add $x $y) somehow becomes of type Syntax
  | _ => none
#check (`(Nat.add 1 1) : Syntax) -- fails, some large type mismatch

Could someone explain what enables this jump in behaviour?

Damiano Testa (Apr 02 2025 at 08:05):

Does it work if you add return?

Damiano Testa (Apr 02 2025 at 08:05):

The syntax quotations are somewhat monadic, so you may have to enable that.

Edward van de Meent (Apr 02 2025 at 08:06):

the weird thing we don't get is that you don't need to write return when matching

Damiano Testa (Apr 02 2025 at 08:07):

Yes, there is some extra voodoo going on there.

Damiano Testa (Apr 02 2025 at 08:07):

For instance, you cannot mix quotations and normal matching.

Edward van de Meent (Apr 02 2025 at 10:07):

does that mean that the notation for matching on syntax quotations is different from the "usual" matching syntax? or just that the elaborator makes this distinction?

Edward van de Meent (Apr 02 2025 at 10:10):

this is really surprising

def isAdd : Syntax  Option (Syntax × Syntax)
  | `(Nat.add $x $y) => some (x, y) -- works, `(Nat.add $x $y) somehow becomes of type Syntax
  | Lean.Syntax.missing => some (.missing, .missing) -- unused variable!!!!!

Edward van de Meent (Apr 02 2025 at 10:11):

so yes, you indeed cannot mix them

Aaron Liu (Apr 02 2025 at 10:21):

Quotations have type [Monad m] [MonadQuotation m] => m (TSyntax _), in order to attach macro scopes and position information to the generated syntax.

Kyle Miller (Apr 02 2025 at 11:09):

There's a special match elaborator that's just for the case when syntax quotations are detected among the patterns. Entry point: docs#Lean.Elab.Term.Quotation.elabMatchSyntax

Eric Wieser (Apr 02 2025 at 11:13):

#check (`(Nat.add 1 1) : Lean.Meta.MetaM Syntax) works

Edward van de Meent (Apr 02 2025 at 11:14):

yea, we figured that much, the confusion was why the match syntax was allowed


Last updated: May 02 2025 at 03:31 UTC