syntax-declarations.lagda.rst

Syntax Declarations

Note

This is a stub

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

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field fst : A
        snd : B fst

syntax Σ A (λ x → B) = [ x ∈ A ] × B

witness : ∀ {A B} → [ x ∈ A ] × B → A
witness (x , _) = x

The syntax declaration for Σ implies that x is in scope in B, but not in A.

You can give fixity declarations along with syntax declarations:

:

infix 5 Σ
syntax Σ A (λ x → B) = [ x ∈ A ] × B

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

Unlike mixfix operators <mixfix-operators> that can be used unapplied using the name including all the underscores, or partially applied by replacing only some of the underscores by arguments, syntax must be fully applied.