tests/lean/1371.lean - third_party/github.com/leanprover/lean4 - Git at Google


            
            def f (stx : Lean.Syntax) :=

            
              match stx with

            
              | `($f $a)  => 1

            
              | `($_)     => 2

            
              | `($f $b)  => 3

            
              | _         => "hello"
	def f (stx : Lean.Syntax) :=
	match stx with
	\| `($f $a) => 1
	\| `($_) => 2
	\| `($f $b) => 3
	\| _ => "hello"