Syntax Declarations

Note

This is a stub

It is now possible to declare user-defined syntax that binds identifiers. Example:

postulate
  State  : Set  Set  Set
  put    :  {S}  S  State S ⊤
  get    :  {S}  State S S
  return :  {A S}  A  State S A
  bind   :  {A B S}  State S B  (B  State S A)  State S A

syntax bind e₁ (λ x  e₂) = x ← e₁ , e₂

increment : State ℕ ⊤
increment = x ← get ,
            put (suc x)

The syntax declaration for bind implies that x is in scope in e₂, but not in e₁.

You can give fixity declarations along with syntax declarations:

infixr 40 bind
syntax bind e₁ (λ x  e₂) = x ← e₁ , e₂

The fixity applies to the syntax, not the name; syntax declarations are also restricted to ordinary, non-operator names. The following declaration is disallowed:

syntax _==_ x y = x === y

Syntax declarations must also be linear; the following declaration is disallowed:

syntax wrong x = x + x

Syntax declarations can have implicit arguments. For example:

id :  {a}{A : Set a} -> A -> A
id x = x

syntax id {A} x = x ∈ A