### Example with Parameters

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Declares an example with explicit and implicit parameters, including type constraints.

```lean
example {G : Type} [Add G] (g : G) : g + g = g + g := rfl
```

--------------------------------

### Noncomputable Example

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Declares a noncomputable example.

```lean
noncomputable example : 2 = 2 := rfl
```

--------------------------------

### Operator Precedence Examples

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Illustrates operator precedence rules in binary expressions, showing how operations are grouped and evaluated. Includes examples with arithmetic and logical operators.

```lean
#eval 4 == 4 - 0
```

```lean
#eval 4 == 3 + 1
```

```lean
#eval 4 == 4 * 1
```

```lean
#eval 4 == 4 / 1
```

```lean
#eval 4 == 4 % 5
```

```lean
example : 4 = 4 - 0 := rfl
```

```lean
example : 4 = 3 + 1 := rfl
```

```lean
example : 4 = 4 * 1 := rfl
```

```lean
example : 4 = 4 / 1 := rfl
```

```lean
example : 4 = 4 % 5 := rfl
```

```lean
#eval false && false || true
```

```lean
#eval true || false && false
```

```lean
#eval 2 ^ 3 * 7 + 2
```

```lean
#eval -2.0 ^ 3 * 7
```

```lean
(module
  (hash_command
    (binary_expression (number) (binary_expression (number) (number))))
  (hash_command
    (binary_expression (number) (binary_expression (number) (number))))
  (hash_command
    (binary_expression (number) (binary_expression (number) (number))))
  (hash_command
    (binary_expression (number) (binary_expression (number) (number))))
  (hash_command
    (binary_expression (number) (binary_expression (number) (number))))
  (declaration
    (example
      type:
        (binary_expression (number) (binary_expression (number) (number)))
      body:
        (identifier)))
  (declaration
    (example
      type:
        (binary_expression (number) (binary_expression (number) (number)))
      body:
        (identifier)))
  (declaration
    (example
      type:
        (binary_expression (number) (binary_expression (number) (number)))
      body:
        (identifier)))
  (declaration
    (example
      type:
        (binary_expression (number) (binary_expression (number) (number)))
      body:
        (identifier)))
  (declaration
    (example
      type:
```

--------------------------------

### Install and Generate tree-sitter CLI Parser

Source: https://context7.com/julian/tree-sitter-lean/llms.txt

Installs the tree-sitter CLI and generates the parser from grammar.js. This is a prerequisite for testing and using the parser.

```bash
# Install tree-sitter CLI
npm install -g tree-sitter-cli

# Generate the parser from grammar.js
tree-sitter generate

# Run the test suite
tree-sitter test

# Parse a specific Lean file
tree-sitter parse example.lean

# Highlight a Lean file (requires queries/highlights.scm)
tree-sitter highlight example.lean
```

--------------------------------

### Example Declaration

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

A simple example declaration in Lean, demonstrating a function application and comparison.

```lean
example : (fun x => x * 2) 4 < 3 = false := rfl
```

--------------------------------

### Namespace With Declarations in Lean

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/organization.txt

An example of a namespace 'Foo' containing two theorem declarations.

```lean
namespace Foo

theorem foo : p := sorry
theorem bar : q := sorry

end Foo
```

```tree-sitter
(module
  (namespace (identifier)
    (declaration (theorem (identifier) (identifier) (sorry)))
    (declaration (theorem (identifier) (identifier) (sorry))) (identifier)))
```

--------------------------------

### Protected Example

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Declares a protected example.

```lean
protected example : 2 = 2 := rfl
```

--------------------------------

### Lean Example with Type Declaration

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Illustrates a Lean example with an explicit type declaration using 'have'. The parsed structure reflects the type annotation and the value.

```lean
example : Nat:=
  have : Type := Nat;
  2
```

```tree-sitter-lean
(module
  (declaration
    (example (identifier) (have (identifier) (identifier) (number)))))
```

--------------------------------

### Simp Tactic With Extra Theorems

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/tactics.txt

Demonstrates using the 'simp' tactic with a list of additional theorems to guide simplification. This allows for more customized simplification strategies.

```lean
example : 2 = 2 := by simp [foo, bar]
```

```tree-sitter-lean
(module
  (declaration
    (example
      type: (binary_expression (number) (number))
      body:
        (tactics
          (simp
            extra: (list (identifier) (identifier)))))))
)
```

--------------------------------

### Install tree-sitter-lean via npm

Source: https://context7.com/julian/tree-sitter-lean/llms.txt

Install tree-sitter-lean as a dependency in your Node.js project for parsing Lean 4 source files programmatically.

```bash
npm install tree-sitter tree-sitter-lean
```

--------------------------------

### Builtin Initialization

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/syntax.txt

Use 'builtin_initialize' for declarations that need to be initialized when the Lean environment is set up. This example shows a basic initialization of 'foo' to 'baz'.

```lean
builtin_initialize foo : bar ←
  baz
```

--------------------------------

### Simple Function Definition and Usage

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Demonstrates a basic function definition and its subsequent usage. No special setup is required.

```lean
def sampleFunction1 x := x*x + 3
```

```lean
def result1 := sampleFunction1 4573
```

```lean
theorem foo : p := sorry
```

--------------------------------

### Tactic Expression Example

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/tactics.txt

Shows how to use a tactic expression with variables defined. This is helpful for interactive theorem proving where context is important.

```lean
variable {m n : Nat}
#check (by
  rewrite Nat.add_comm
  exact (Nat.left_distrib 2 n m).symm : 2 * m + 2 * n = 2 * (n + m))
```

```tree-sitter-lean
(module
  (variable
    (implicit_binder
      name: (identifier)
      name: (identifier)
      type: (identifier)))
  (hash_command
    (parenthesized
      (tactics (rewrite (identifier))
        (term
          (proj
            term:
              (parenthesized
                (apply
                  name: (identifier)
                  arguments: (number)
                  arguments: (identifier)
                  arguments: (identifier)))
            name: (identifier))))
      (type_ascription
        type:
          (binary_expression
            (binary_expression
              (binary_expression (number) (identifier))
              (binary_expression (number) (identifier)))
            (binary_expression
              (number)
              (parenthesized
                (binary_expression (identifier) (identifier)))))))))
```

--------------------------------

### Declare Syntax

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/syntax.txt

Declare custom syntax for specific terms or tactics. This example declares 'foo' and 'str' as tactics.

```lean
syntax "foo" : tactic
syntax str : tactic
```

--------------------------------

### Theorem with Match Body in Lean

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Demonstrates a theorem in Lean with a match expression as its body. This example uses pattern matching on tuples and includes a `sorry` placeholder for the proof.

```lean
theorem foo {p : α × β} :
  p = p ↔ p = p
  | (p1, p2), (q1, q2) => sorry
```

--------------------------------

### Generate and Test Tree-sitter Grammar

Source: https://github.com/julian/tree-sitter-lean/blob/main/README.rst

Run these commands to generate the parser and execute tests for the grammar. Ensure you have the tree-sitter CLI installed.

```sh
$ tree-sitter generate && tree-sitter test
```

--------------------------------

### Nested If-Then-Else

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/do.txt

Demonstrates nested `if-then-else` structures. This example shows how conditional logic can be chained.

```Lean
#check if true then do if false then false else false else true
```

```tree-sitter-lean
(module
  (hash_command
    (if_then_else
      (true)
      (do (if_then_else (false) (false) (false)))
      (true))))
```

--------------------------------

### Check Failure Example

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/commands.txt

Illustrates a #check command that is expected to fail, showing a complex type assertion.

```lean
#check_failure (inferInstance : Inhabited (Nat × _))
```

--------------------------------

### Parse Lean 4 code in Rust

Source: https://context7.com/julian/tree-sitter-lean/llms.txt

Use the `language()` function to get the Tree-sitter Language object for Lean 4 and configure a parser instance to parse Lean 4 source code. This example demonstrates parsing a simple Lean definition and theorem, then printing the root node kind and traversing its children.

```rust
use tree_sitter::Parser;
use tree_sitter_lean::language;

fn main() {
    let code = r#"def add (x y : Nat) : Nat := x + y

theorem add_comm (a b : Nat) : add a b = add b a := by
  simp [add, Nat.add_comm]
"#;

    let mut parser = Parser::new();
    parser.set_language(language()).expect("Error loading Lean grammar");

    let tree = parser.parse(code, None).unwrap();
    let root_node = tree.root_node();

    println!("Root node kind: {}", root_node.kind());
    println!("Child count: {}", root_node.child_count());

    // Traverse the syntax tree
    for child in root_node.children(&mut root_node.walk()) {
        println!("  {} [{}-{}]", child.kind(), child.start_position().row, child.end_position().row);
    }
}

```

--------------------------------

### Unknown User Tactic

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/tactics.txt

An example demonstrating the parsing of custom or unknown tactics within a Lean proof. This shows the flexibility of the grammar in handling arbitrary tactic sequences.

```lean
example : true ↔ true := by
  foo
  bar baz
  baz
```

```tree-sitter-lean
(module
  (declaration
    (example (binary_expression (true) (true))
      (tactics
        (identifier)
        (apply (identifier) (identifier))
        (identifier)))))
)
```

--------------------------------

### Elaborate Term

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/syntax.txt

Use the 'elab' command to define custom elaboration logic for terms. This example elaborates a term 'foo' into 'Lean.Elab.Term.elabTerm x none'.

```lean
elab "foo" x:term : term => Lean.Elab.Term.elabTerm x none
```

--------------------------------

### Simp Tactic

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/tactics.txt

A basic example of using the 'simp' tactic to simplify expressions. This is a fundamental tactic for automated reasoning.

```lean
example : 2 = 2 := by simp
```

```tree-sitter-lean
(module
  (declaration
    (example (binary_expression (number) (number)) 
      (tactics (simp)))))
)
```

--------------------------------

### Define Macro

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/syntax.txt

Define a macro that expands to a specific code snippet. This example defines a macro named 'foo' that expands to 'trivial'.

```lean
macro "foo" : tactic => `(trivial)
```

--------------------------------

### Parse Lean Structures and Classes

Source: https://context7.com/julian/tree-sitter-lean/llms.txt

Parse Lean structure and class declarations, including fields, default values, and inheritance. This example shows how to extract structure names and field information.

```lean
-- Lean source to parse:
structure Point (α : Type u) where
  x : α
  y : α
  z : α := 0

class Monoid (M : Type) extends Semigroup M where
  one : M
  one_mul : ∀ a, one * a = a
  mul_one : ∀ a, a * one = a

```

```javascript
const code = `
structure Point (α : Type u) where
  w : String := "default"
  x : α
  y : Foo Bar Baz
`;

const tree = parser.parse(code);
const structure = tree.rootNode.descendantsOfType('structure')[0];

console.log('Structure name:', structure.childForFieldName('name').text);
// Output: Structure name: Point

// Get fields
const fields = structure.children.filter(c => c.type === 'field');
for (let field of fields) {
    const name = field.childForFieldName('name');
    const defaultVal = field.childForFieldName('default');
    console.log(`Field: ${name?.text}, has default: ${!!defaultVal}`);
}
// Output:
// Field: w, has default: true
// Field: x, has default: false
// Field: y, has default: false

```

--------------------------------

### Theorem with Expression Body in Lean

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Defines a theorem in Lean with an expression as its body. This example uses `Nat.mul_comm` to prove the commutativity of multiplication.

```lean
theorem bar : 2 * 3 = 3 * 2 := Nat.mul_comm 2 3
```

--------------------------------

### Range with Step

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Defines a range with explicit start, stop, and step values. Used for sequence generation.

```lean
#check [0:foo 3:1]
```

--------------------------------

### Basic Function Definition with Return

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/do.txt

Defines a simple function `f` that returns a Nat value. This is a fundamental example of function declaration in Lean.

```Lean
def f : Nat := do
  return 3
```

```tree-sitter-lean
(module
  (declaration
    (def (identifier) (identifier) (do (do_return (number))))))
```

--------------------------------

### Parse Lean 4 code in Node.js

Source: https://context7.com/julian/tree-sitter-lean/llms.txt

Use the Node.js binding to parse Lean 4 source code with the tree-sitter npm package. This example parses a function definition and an `#eval` command, then prints the syntax tree structure and demonstrates a recursive walk through the tree nodes.

```javascript
const Parser = require('tree-sitter');
const Lean = require('tree-sitter-lean');

const parser = new Parser();
parser.setLanguage(Lean);

const sourceCode = `
def twice (f : Nat → Nat) (a : Nat) := f (f a)

#eval twice (fun x => x + 2) 10
`;

const tree = parser.parse(sourceCode);

console.log(tree.rootNode.toString());
// Output: (module (declaration (def name: (identifier) (binders (explicit_binder name: (identifier) type: (arrow (identifier) (identifier))) (explicit_binder name: (identifier) type: (identifier))) body: (apply name: (identifier) arguments: (parenthesized (apply name: (identifier) arguments: (identifier)))))) (hash_command (apply (identifier) (parenthesized (fun (parameters (identifier)) (binary_expression (identifier) (number)))) (number))))

// Query specific nodes
function walkTree(node, depth = 0) {
    const indent = '  '.repeat(depth);
    console.log(`${indent}${node.type} [${node.startPosition.row}:${node.startPosition.column}]`);
    for (let child of node.children) {
        walkTree(child, depth + 1);
    }
}

walkTree(tree.rootNode);

```

--------------------------------

### Define Macro Rules

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/syntax.txt

Macro rules allow for pattern matching and transformation of code. This example defines two macro rules: one for 'tactic| foo' and another for 'tactic| bar'.

```lean
macro_rules
  | `(tactic| foo) => `(tactic|trivial)
  | `(tactic| bar) => `(tactic|apply foo bar)
```

--------------------------------

### Prelude and Import

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/commands.txt

Demonstrates the 'prelude' keyword and importing a module named 'Foo'.

```lean
prelude
import Foo
```

--------------------------------

### Basic Commands

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/commands.txt

Demonstrates basic commands like #check, #eval, #reduce, and #print with simple expressions and identifiers.

```lean
#check 2+2
#eval 2+2
#reduce 2+2
#print inferInstance
```

--------------------------------

### Define Custom Notation

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/syntax.txt

Use custom notations to define custom symbols or keywords for specific meanings within your Lean code. This example shows a simple notation for '♔'.

```lean
notation " ♔ " => Foo.bar
```

--------------------------------

### Apply Tactic

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/tactics.txt

Shows how to use the 'apply' tactic to introduce a specific theorem or constructor, such as 'Iff.intro' for proving biconditionals. This is useful for breaking down complex goals.

```lean
example : true ↔ true := by apply Iff.intro
```

```tree-sitter-lean
(module
  (declaration
    (example (binary_expression (true) (true))
      (tactics (apply_tactic (identifier))))))
)
```

--------------------------------

### Intro Tactic

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/tactics.txt

Illustrates the use of the 'intro' tactic to introduce variables into a quantified statement, followed by 'rfl' for reflexivity. This is common for proving universal quantifiers.

```lean
example : ∀ x y : Nat, x + y = x + y := by
  intro x y
  rfl
```

```tree-sitter-lean
(module
  (declaration
    (example
      (forall
        (binders
          (identifier)
          (identifier)
          (identifier))
        (binary_expression
          (binary_expression
            (identifier)
            (identifier))
          (binary_expression
            (identifier)
            (identifier))))
      (tactics
        (intro
          (identifier)
          (identifier))
        (rfl)))))
)
```

--------------------------------

### Range without Start

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Defines a range specifying only the stop value. The start is implicitly 0.

```lean
#check [:3]
```

--------------------------------

### Open Namespace

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/commands.txt

Shows different ways to open namespaces, including nested ones.

```lean
open Foo
open Foo.Bar
open Foo Bar Baz.Quux
```

--------------------------------

### Instance Definition

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Provides an instance of 'ToString' for 'Foo', defining the 'toString' method.

```lean
instance : ToString Foo where
  toString (d : Foo) : String := "Foo"
```

```lean
(module
  (declaration
    (instance
      type:
        (apply
          name: (identifier)
          arguments: (identifier))
      body:
        (where_decl
          name: (identifier)
          binders:
            (explicit_binder
              name: (identifier)
              type: (identifier))
          type: (identifier)
          body: (string)))))

```

--------------------------------

### Let Bindings (Assignment)

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/do.txt

Demonstrates parsing of 'let' bindings in Lean, including assignments with '<-' and '<--' operators, and direct assignment with ':='.

```lean
def f : Unit := do
  let c <- 2
  let d ← 2
  let e := 2
```

```tree-sitter-lean
(module
  (declaration
    (def (identifier) (identifier)
    (do
      (let_bind (identifier) (number))
      (let_bind (identifier) (number))
      (let (identifier) (number))))))
```

--------------------------------

### Subarray Slice without Start

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Extracts a slice from an array from the beginning up to a specified index.

```lean
#check foo[:3]
```

--------------------------------

### Same Line Commands

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/commands.txt

Shows how multiple commands can be placed on the same line, separated by spaces.

```lean
#eval id 2 #eval 5
```

--------------------------------

### Instance with Field Definition

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Defines an instance for 'Add Foo' by assigning 'Foo.add' to the default field.

```lean
instance : Add Foo := Foo.add
```

```lean
(module
  (declaration
    (instance
      type:
        (apply
          name: (identifier)
          arguments: (identifier))
      body: (identifier)))))

```

--------------------------------

### Subarray Slice without Stop

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Extracts a slice from an array starting at a specified index up to the end.

```lean
#check foo[0:]
```

--------------------------------

### Range without Step

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Defines a range with only start and stop values. The step is implicitly 1.

```lean
#check [0:10]
```

--------------------------------

### Match Syntax Sugar

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Demonstrates the use of Lean's match syntax sugar for pattern matching on different cases. Requires understanding of pattern matching.

```lean
def foo : Nat → Nat
  | 0 => 2
  | 2 => 3
  | _ => 5
```

--------------------------------

### Subarray Slice

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Extracts a slice from an array with specified start and stop indices. The stop index is exclusive.

```lean
#check foo[0:bar 3]
```

--------------------------------

### Instance with Parameters

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Defines an instance for 'Quux' with implicit and explicit parameters 'f' and 'g'.

```lean
instance {f : Foo} (g : Bar 3) : Quux where
  foo := f
```

```lean
(module
  (declaration
    (instance
      (binders
        (implicit_binder
          name: (identifier)
          type: (identifier))
        (explicit_binder
          name: (identifier)
          type:
            (apply
              name: (identifier)
              arguments: (number))))
      type: (identifier)
      body:
        (where_decl
          name: (identifier)
          body: (identifier)))))

```

--------------------------------

### Open In Declaration

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/commands.txt

Demonstrates opening a namespace and then defining a local variable within that scope.

```lean
open Foo in
  def baz := bar
```

--------------------------------

### Open Command (Missing Name)

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/commands.txt

Represents an 'open' command without a specified namespace, which is syntactically incorrect.

```lean
open
```

--------------------------------

### Lean Lift Method Syntax

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Demonstrates the syntax for the 'lift' method in Lean, typically used for type conversions or lifting operations.

```lean
#check ← Nat
```

--------------------------------

### Variable Declarations in Lean

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/organization.txt

Demonstrates various ways to declare variables, including typed, untyped, implicit, and instance binders.

```lean
variable (α β γ : Type)
variable (g : β → γ) (f : α → β) (h : α → α)
variable {x : α} [y : α]
```

```tree-sitter
(module
  (variable
    (explicit_binder
      name: (identifier)
      name: (identifier)
      name: (identifier)
      type: (identifier)))
  (variable
    (explicit_binder
      name: (identifier)
      type: (arrow (identifier) (identifier)))
    (explicit_binder
      name: (identifier)
      type: (arrow (identifier) (identifier)))
    (explicit_binder
      name: (identifier)
      type: (arrow (identifier) (identifier))))
  (variable
    (implicit_binder
      name: (identifier)
      type: (identifier))
    (instance_binder
      name: (identifier)
      type: (identifier))))
```

--------------------------------

### Match Multiple Arguments

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Shows how to use match expressions with multiple arguments.

```lean
def foo (a b c : Nat) :=
  match a, b, c with
  | _, _, _ => true
```

--------------------------------

### Lean Definition with Let Binding

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Demonstrates a Lean function definition using a local let binding. The parsed output shows the structure of the definition and the binding.

```lean
def foo :=
  let foo <- 12
  foo
```

```tree-sitter-lean
(module
  (declaration
    (def
      name: (identifier)
      (ERROR (identifier))
      body:
        (apply
          name: (lift_method (number))
          arguments: (identifier)))))
```

--------------------------------

### Subarray Slice with Invalid Copy

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Shows an invalid subarray slice syntax using a colon without start or stop indices.

```lean
#check foo[:]
```

--------------------------------

### Theorem Proof by Reflexivity in Lean

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Illustrates a theorem declaration in Lean with a proof by reflexivity. The `rfl` tactic is used to prove equality by showing both sides are definitionally equal.

```lean
theorem twiceAdd2 (a : Nat) : twice (fun x => x + 2) a = a + 4 :=
-- The proof is by reflexivity. Lean "symbolically" reduces both sides of the equality
-- until they are identical.
  rfl
```

--------------------------------

### Instance Declaration with Do Block

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/do.txt

Defines an instance for `ToString Nat` using a `do` block. This demonstrates how `do` notation can be used within instance definitions.

```Lean
instance : do return ToString Nat where
  toString (d : Nat) : String := "Foo"
```

```tree-sitter-lean
(module
  (declaration
    (instance
      type:
        (do
          (do_return
            value:
              (apply
                name: (identifier)
                arguments: (identifier))))
      body:
        (where_decl
          name: (identifier)
          binders:
            (explicit_binder
              name: (identifier)
              type: (identifier))
          type: (identifier)
          body: (string)))))
```

--------------------------------

### Define Mixfix Operators

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/syntax.txt

Define mixfix operators (prefix, infix, infixl, infixr, postfix) with a specified binding precedence. This example defines several operators using the symbol '↑'.

```lean
prefix:max "↑" => coe
infix:max "↑" => coe
infixl:max "↑" => coe
infixr:max "↑" => coe
postfix:max "↑" => coe
```

--------------------------------

### Class Definition with Fields and Parameters

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Defines a class 'Quux' with a type parameter 'a', fields like 'foo', 'add', 'bar', and 'baz'.

```lean
class Quux (a : Type) where
  foo : String := "foo"
  add : a -> a -> a
  bar := 0
  baz {x : String} : String
```

```lean
(module
  (declaration
    (structure
      name: (identifier)
      (binders
        (explicit_binder
          name: (identifier)
          type: (identifier)))
      fields:
        (field
          name: (identifier)
          type: (identifier)
          default: (string))
      fields:
        (field
          name: (identifier)
          type: (arrow (identifier) (arrow (identifier) (identifier))))
      fields:
        (field
          name: (identifier)
          default: (number))
      fields:
        (field
          name: (identifier)) fields: (implicit_binder name: (identifier) type: (identifier)) (ERROR) fields: (field name:
          (identifier)))))
```

--------------------------------

### Match Multiple With Apply

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Demonstrates match expressions combined with function application.

```lean
#eval match 0 with
| 0 => id 2
| _ => id 4
```

--------------------------------

### Multiple Function Arguments

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Shows how to pass multiple arguments to a function in Lean.

```lean
#check foo 2 3 4
```

--------------------------------

### Access Lean 4 Node Types in Rust

Source: https://context7.com/julian/tree-sitter-lean/llms.txt

Utilize the `NODE_TYPES` constant, which contains the JSON schema for Lean 4 grammar node types, to build tooling. This example parses the JSON and lists all named node types available in the grammar.

```rust
use tree_sitter_lean::NODE_TYPES;

fn main() {
    // Parse the node types JSON for tooling purposes
    let node_types: serde_json::Value = serde_json::from_str(NODE_TYPES).unwrap();

    // List all named node types
    if let Some(types) = node_types.as_array() {
        for node_type in types {
            if let Some(name) = node_type.get("type").and_then(|t| t.as_str()) {
                let named = node_type.get("named").and_then(|n| n.as_bool()).unwrap_or(false);
                if named {
                    println!("Node type: {}", name);
                }
            }
        }
    }
}

```

--------------------------------

### Basic String Literals

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/strings.txt

Demonstrates the parsing of basic string literals, including empty strings and strings with single quotes.

```lean
#eval "foo"
#eval "'"
```

```lean
#eval ""
```

--------------------------------

### Named Arguments

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Demonstrates the usage of named arguments in Lean function calls.

```lean
#check foo (bar := 3)
```

--------------------------------

### If-Then-Else Syntax

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Demonstrates the basic if-then-else structure. This is used for conditional execution.

```lean
#eval if true then "foo"
```

```lean
(module (hash_command (if_then_else (true) (string) (string))))
```

--------------------------------

### Multimatch Syntax Sugar in Lean

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Demonstrates Lean's multimatch syntax for function definitions with multiple patterns. This syntax allows for concise definition of functions based on different input cases.

```lean
def foo : Nat → Nat -> Nat
  | 0, foo => 2
  | 2, bar => 3
  | _, _ => 5
```

--------------------------------

### Import Nested Module

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/commands.txt

Shows how to import a deeply nested module.

```lean
import Foo.Bar.Baz
```

--------------------------------

### Application with Parentheses and Dollar Operator

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Shows different ways to apply functions, including nested calls and the '$' operator for precedence.

```lean
#eval foo bar (baz (1 + 1))
```

```lean
#eval foo bar $ baz (1 + 1)
```

```lean
#eval foo bar $ baz $ 1 + 1
```

--------------------------------

### Function with Type Ascription and Return

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/do.txt

Shows a function that returns `PUnit.unit` and includes a type ascription. This is useful for ensuring type correctness.

```Lean
#check (do return PUnit.unit : PUnit)
```

```tree-sitter-lean
(module
  (hash_command
    (parenthesized
      (do
        (do_return
          value: (identifier)))
      (type_ascription
        type: (identifier)))))
```

--------------------------------

### Multiple Let Bindings with Semicolons

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Defines multiple local variables using let bindings, separated by semicolons. Suitable for sequential assignments.

```lean
def foo :=
let foo := 12
let bar := 13
let baz := 14
foo + bar + baz
```

```lean
def bar :=
let foo := 12;
let bar := 13;
let baz := 14;
foo + bar + baz
```

```lean
def baz :=
let foo := 12; let bar := 13; let baz := 14;
foo + bar + baz
```

--------------------------------

### Product Type Precedence

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Illustrates the precedence rules for product types in Lean, showing how they interact with function application.

```lean
#check f 3 × C
```

--------------------------------

### Parse Lean Theorems and Proofs

Source: https://context7.com/julian/tree-sitter-lean/llms.txt

Parse theorems with tactic-based proofs using the `by` keyword. This snippet demonstrates accessing theorem names and identifying tactics within the proof.

```lean
-- Lean source to parse:
theorem add_comm_example {m n : Nat} : m + n = n + m := by
  rewrite Nat.add_comm
  rfl

example : ∀ x y : Nat, x + y = x + y := by
  intro x y
  rfl

```

```javascript
const code = `
theorem foo {m n : Nat} : 2 * m + 2 * n = 2 * (n + m) := by
  rewrite Nat.add_comm
  exact (Nat.left_distrib 2 n m).symm
`;

const tree = parser.parse(code);
const theorem = tree.rootNode.descendantsOfType('theorem')[0];

console.log('Theorem name:', theorem.childForFieldName('name').text);
// Output: Theorem name: foo

// Find tactics in the proof
const tactics = tree.rootNode.descendantsOfType('tactics')[0];
for (let tactic of tactics.children) {
    if (tactic.isNamed) {
        console.log('Tactic:', tactic.type, '-', tactic.text.substring(0, 30));
    }
}
// Output:
// Tactic: rewrite - rewrite Nat.add_comm
// Tactic: term - exact (Nat.left_distrib 2 n m

```

--------------------------------

### Universes Command (Incorrect Syntax)

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/commands.txt

Shows an incorrect usage of the 'universes' keyword, which is not a valid command in this context.

```lean
universes u2 v2 w2
```

--------------------------------

### Subarray vs. Range Syntax

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Illustrates the distinction between subarray indexing and range notation in Lean.

```lean
#check foo [1:2]
```

--------------------------------

### Named Instance Definition

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Defines a named instance 'toStringFoo' for 'ToString Foo', specifying the 'toString' implementation.

```lean
instance toStringFoo : ToString Foo where
  toString (d : Foo) : String := "Foo"
```

```lean
(module
  (declaration
    (instance
      name: (identifier)
      type:
        (apply
          name: (identifier)
          arguments: (identifier))
      body:
        (where_decl
          name: (identifier)
          binders:
            (explicit_binder
              name: (identifier)
              type: (identifier))
          type: (identifier)
          body: (string)))))

```

--------------------------------

### Universe Command (Missing Name)

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/commands.txt

Represents a 'universe' command without any universe parameters, which is syntactically incorrect.

```lean
universe
```

--------------------------------

### Anonymous Function via Lambda

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Demonstrates the lambda syntax `λ` for creating anonymous functions. The body can be a simple identifier.

```lean
(module
  (hash_command
    (fun (parameters (identifier)) (identifier))))
```

--------------------------------

### Integrate tree-sitter-lean with Neovim

Source: https://context7.com/julian/tree-sitter-lean/llms.txt

Configures nvim-treesitter to enable syntax highlighting and indentation for Lean files in Neovim. Optionally integrates with lean.nvim for enhanced IDE features.

```lua
-- In your Neovim config (init.lua or similar)
require('nvim-treesitter.configs').setup {
  ensure_installed = { "lean" },
  highlight = {
    enable = true,
  },
  indent = {
    enable = true,
  },
}

-- Or use with lean.nvim for full Lean 4 IDE support
require('lean').setup {
  lsp = { on_attach = on_attach },
  mappings = true,
}
```

--------------------------------

### Structure Without Fields

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Defines an empty structure 'Foo'.

```lean
structure Foo where
```

```lean
(module
  (declaration
    (structure
      name: (identifier))))

```

--------------------------------

### Structure Extension in Lean

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Illustrates structure extension in Lean. `Bar` extends `Foo`, and `Baz` extends `Quux`, demonstrating inheritance of fields.

```lean
structure Bar extends Foo where
  bit : Bool

class Baz extends Quux where
  bit : Bool
```

--------------------------------

### Comparison Operators

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Demonstrates the use of various comparison operators in Lean.

```lean
#check 2 < 3
```

```lean
#check 2 ≤ 3
```

```lean
#check 2 <= 3
```

```lean
#check 2 > 3
```

```lean
#check 2 ≥ 3
```

```lean
#check 2 >= 3
```

--------------------------------

### Try-Catch-Finally Block

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/do.txt

Illustrates exception handling using `try`, `catch`, and `finally` blocks. This is essential for robust IO operations.

```Lean
def f : IO Unit := do try println! "foo" catch ex => throw ex finally println! "bar"
```

```tree-sitter-lean
(module
  (declaration
    (def (identifier) (apply (identifier) (identifier))
    (do
      (try
        (apply (identifier) (string))
        (catch (identifier)
          (throw (identifier)))
        (finally (apply (identifier) (string))))))))
```

--------------------------------

### Instance with Match Syntax Sugar

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Defines an instance of the ToString typeclass for Foo, using match syntax for pattern matching.

```lean
instance : ToString Foo where
  toString
  | _ => "foo"
```

--------------------------------

### Quoted Command Syntax

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/commands.txt

Demonstrates defining a command within a quoted string literal, allowing for complex nested structures.

```lean
def f : Lean.Elab.Command.CommandElabM Lean.Syntax :=
`( 
    namespace bar
    def bar := 12
    end bar
  )
```

--------------------------------

### Multiple Let Bindings (Lean AST)

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Represents multiple sequential let bindings within a definition in the Lean AST. Each binding is processed in order.

```tree-sitter-lean
(module
  (declaration
    (def (identifier)
      (let
        (identifier)
        (number)
        (let
          (identifier)
          (number)
          (let
            (identifier)
            (number)
            (binary_expression
              (binary_expression (identifier) (identifier))
              (identifier)))))))
  (declaration
    (def (identifier)
      (let
        (identifier)
        (number)
        (let
          (identifier)
          (number)
          (let
            (identifier)
            (number)
            (binary_expression
              (binary_expression (identifier) (identifier))
              (identifier)))))))
  (declaration
    (def (identifier)
      (let
        (identifier)
        (number)
        (let
          (identifier)
          (number)
          (let
            (identifier)
            (number)
            (binary_expression
              (binary_expression (identifier) (identifier))
              (identifier)))))))
  (declaration
    (def (identifier)
      (let
        (identifier)
        (number)
        (let
          (identifier)
          (number)
          (let
            (identifier)
            (number)
            (binary_expression
              (binary_expression (identifier) (identifier))
              (identifier))))))))
```

--------------------------------

### Empty Class Definition

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Defines an empty class 'Foo'.

```lean
class Foo where
```

```lean
(module
  (declaration
    (structure
      name: (identifier))))

```

--------------------------------

### Import Command (Missing Name)

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/commands.txt

Represents an 'import' command without a specified module name, which is syntactically incorrect.

```lean
import
```

--------------------------------

### AST for Match Syntax with Anonymous Function

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Shows the AST for Lean code using match syntax within an anonymous function. This helps in parsing complex lambda expressions with pattern matching.

```lean
(module
  (declaration
    (def
      name: (identifier)
      type: (arrow (identifier) (identifier))
      body:
        (fun
          lhs: (number)
          (true)
          lhs: (hole)
          (false)))))
```

--------------------------------

### Try/Catch Block

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/do.txt

Parses a Lean 'try/catch' block, demonstrating how to handle exceptions. The 'catch' block specifies the exception variable and the action to take.

```lean
def f : IO Unit := do
  try
    println! "foo"
  catch ex =>
    throw ex
```

```tree-sitter-lean
(module
  (declaration
    (def (identifier) (apply (identifier) (identifier))
    (do
      (try
        (apply (identifier) (string))
        (catch (identifier)
          (throw (identifier))))))))
```

--------------------------------

### Lean Borrowed Type Syntax

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Demonstrates the syntax for borrowing a type in Lean, indicated by the '@&' prefix.

```lean
#check @& String
```

--------------------------------

### Bare Parameters Function Let Binding (Lean AST)

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Represents a local function with bare parameters in a let binding within the Lean AST. Parameters are listed without explicit types.

```tree-sitter-lean
(module
  (declaration
    (def
      name: (identifier)
      body:
        (let
          name: (identifier)
          parameters:
            (parameters
              name: (identifier)
              name: (identifier))
          value: (number)
          body:
            (apply
              name: (identifier)
              arguments: (true)
              arguments: (false))))))
```

--------------------------------

### Mixed Named Arguments

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Illustrates calling a function with a mix of positional and named arguments.

```lean
#check foo 1 (bar := 3) 2 (baz := 4)
```

--------------------------------

### Multiple Let Bindings without Semicolons

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Defines multiple local variables using let bindings, without semicolons. Each binding is on a new line.

```lean
def quux :=
  let foo := 12
  let bar := 13
  let baz := 14
  foo + bar + baz
```

--------------------------------

### Lean Universal and Existential Quantifiers

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Shows how universal (∀) and existential (∃) quantifiers are represented in Lean syntax, including nested quantifiers and binders with types.

```lean
#check ∀ x, ∃ y, x + y = x
```

```lean
#check ∃ (x y : Nat), ∀ w, w + x + y + z = x
```

--------------------------------

### Instance with Inductive Constructor

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Provides an instance for 'Inhabited Nat' using an anonymous constructor with the value '0'.

```lean
instance : Inhabited Nat := ⟨0⟩
```

```lean
(module
  (declaration
    (instance
      type:
        (apply
          name: (identifier)
          arguments: (identifier))
      body: (anonymous_constructor (number)))))

```

--------------------------------

### Partial Definition

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Defines a partial function 'foo' which is not guaranteed to terminate.

```lean
partial def foo := 12
```

--------------------------------

### Match Syntax with Anonymous Function

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Combines Lean's match syntax sugar with an anonymous function (fun). This showcases concise function definitions with pattern matching.

```lean
def foo : Nat -> Bool :=
  fun
    | 0 => true
    | _ => false
```

--------------------------------

### Section With Declarations in Lean

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/organization.txt

A section 'Foo' that includes two theorem declarations.

```lean
section Foo

theorem foo : p := sorry
theorem bar : q := sorry

end Foo
```

```tree-sitter
(module
  (section (identifier)
    (declaration (theorem (identifier) (identifier) (sorry)))
    (declaration (theorem (identifier) (identifier) (sorry))) (identifier)))
```

--------------------------------

### Product Type (Tuple)

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Represents a product type, often used for tuples, with elements separated by commas.

```lean
#check (10, "foo", 30, 40)
```

--------------------------------

### Nested Empty Namespace in Lean

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/organization.txt

Demonstrates a nested namespace structure where 'Bar' is nested within 'Foo'.

```lean
namespace Foo
namespace Bar
end Bar
end Foo
```

```tree-sitter
(module
  (namespace (identifier)
    (namespace (identifier) (identifier)) (identifier)))
```

--------------------------------

### Lean Subtype Syntax

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Illustrates the syntax for defining subtypes in Lean, using curly braces `{}` with a condition.

```lean
#check {x // x > 2}
```

--------------------------------

### Interpolation With Escape Sequences

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/strings.txt

Demonstrates string interpolation that also includes various escape sequences within the string.

```lean
#eval s!"f\'o\"\ro\nb\ta\\r {baz}"
```

--------------------------------

### Noncomputable Instance

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Defines a noncomputable instance of 'Foo'.

```lean
noncomputable instance : Foo where x := 2
```

--------------------------------

### Instance Field with Function Return Type

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Defines an instance for 'ToString Foo' with 'toString' having an explicit return type and a lambda function body.

```lean
instance : ToString Foo where
  toString : Foo → String := λ f => s!"Foo"
```

```lean
(module
  (declaration
    (instance
      type:
        (apply
          name: (identifier)
          arguments: (identifier))
      body:
        (where_decl
          name: (identifier)
          type: (arrow (identifier) (identifier))
          body:
            (fun
              (parameters name: (identifier))
              (interpolated_string))))))

```

--------------------------------

### AST for Multi-Argument Annotated Function

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Shows the AST for a function with multiple annotated arguments. Useful for understanding how multiple binders are represented.

```lean
(module
  (declaration
    (def
      name: (identifier)
      (binders
        (explicit_binder
          name: (identifier)
          name: (identifier)
          type: (identifier)))
      body:
        (binary_expression (identifier) (identifier))))
```

--------------------------------

### Negation with Comments

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/expressions.txt

Demonstrates the use of double hyphens for comments in conjunction with negation. This syntax is specific and should be used carefully.

```lean
#eval --2
```

```lean
#eval --foo
```

```lean
(module (ERROR (comment) (comment)))
```

--------------------------------

### Function Let Binding (Lean AST)

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Represents a local function definition within a let binding in the Lean AST. Includes parameters, value, and body.

```tree-sitter-lean
(module
  (declaration
    (def
      name: (identifier)
      type: (identifier)
      body:
        (let
          name: (identifier)
          parameters:
            (parameters
              (explicit_binder
                name: (identifier)
                name: (identifier)
                type: (identifier)))
          value: (binary_expression (identifier) (identifier))
          body:
            (apply
              name: (identifier)
              arguments: (identifier)
              arguments: (number)
              arguments: (number))))))
```

--------------------------------

### AST for Typeclass Resolved Arguments

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Shows the AST for a Lean function using typeclass instances. This helps in understanding how instance arguments are parsed.

```lean
(module
  (declaration
    (def
      name: (identifier)
      (binders
        (instance_binder
          type:
            (apply
              name: (identifier)
              arguments: (identifier)))
        (instance_binder
          name: (identifier)
          type: (identifier)))
      type: (identifier)
      body: (number))))
```

--------------------------------

### AST for Annotated Function Definition

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Illustrates the AST for a Lean function with an annotated argument. This helps in parsing and analyzing functions with explicit types.

```lean
(module
  (declaration
    (def
      name: (identifier)
      (binders
        (explicit_binder
          name: (identifier)
          type: (identifier)))
      body:
        (binary_expression
          (binary_expression
            (binary_expression
            (binary_expression (number) (identifier))
              (identifier))
              (identifier))
          (number))))
```

--------------------------------

### Annotated Let Binding (Lean AST)

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Represents an annotated let binding in the Lean Abstract Syntax Tree (AST). Includes the identifier, type, value, and body.

```tree-sitter-lean
(module
  (declaration
    (def
      name: (identifier)
      body:
        (let
          name: (identifier)
          type: (identifier)
          value: (number)
          body: (identifier)))))
```

--------------------------------

### AST for First-Class Function

Source: https://github.com/julian/tree-sitter-lean/blob/main/test/corpus/declarations.txt

Illustrates the AST for a higher-order function definition in Lean. This is useful for parsing functions that manipulate other functions.

```lean
(module
  (declaration
    (def
      name: (identifier)
      (binders
        (explicit_binder
          name: (identifier)
          type: (arrow (identifier) (identifier)))
        (explicit_binder
          name: (identifier)
          type: (identifier)))
      body:
        (apply
          name: (identifier)
          arguments:
            (parenthesized
              (apply
                name: (identifier)
                arguments: (identifier)))))))
```