## Syntax and Semantics

### Quotations & Anti-quotations

#### Identifiers

```
@x = ident:(x)
&x
= hyp @x (in ltac2 expressions)
= ltac2:(Control.refine (fun () => hyp @x)) (in constrs)
```

#### Constrs / Terms

```
'term = open_constr:(term)
```

#### Anti-quotation

```
$x = ltac2:(Control.refine (fun () => x)) (with x : constr)
```

An extra explanation for anti-quotation semantics.

… the semantics of the quotation is to evaluate its content inside a goal Γ ⊢ A where Γ is the current list of hypotheses, and A the inferred type of the hole. … This is precisely the role of

`Control.refine : (unit -> constr) -> unit`

. It takes a (for technical reasons, thunked) term as an argument and uses it to solve the goal(s) under focus.

## Notations

### Syntactic Classes

```
tactic(n) where n = 0 .. 6
```

`n = 0`

: atoms, parenthesized expression, list / record / unit literals`n = 1`

: function application, record field access (?)`n = 2`

: list cons`n = 3`

: comma expression (?)`n = 4`

:`n = 5`

: let binding, lambda expression`n = 6`

: tactic sequence (`;`

expression)