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)

complete grammar

Idioms