Search code examples
coq

Curly brace proof syntax: begin x. = { auto } y. []

I've seen the following syntax used in Coq proofs, with variations to the relation (=) and the tactic (auto):

begin
  x.
= { auto }
  y.
= { auto }
  z.
[].

What's the name of this syntactic construct, and where is it documented?

Solution

  • This seems to be a tactic notation defined by the project you linked. Here is the file defining the notation, starting at Line 84.