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