syn250113

id = ...
c = id: e
m = id%.
e = primitive
  | λ( (id* | id*: e)%, ) e
  | λ{ (id* | id*: e)%, } e
  | Π( (e | id*: e)%, ) e
  | Π{ (e | id*: e)%, } e
  | e e
  | e {e}
  | ( e%, )
  | { (id (id* | {id*} | (id*: e) | {id*: e})*[: e] = e)%, }
  | Σ( (e | id*: e)%, )
  | Σ{ (id*: e)%, }
  | e.nat
  | e.id
  | σ{ (id (id* | {id*} | (id*: e) | {id*: e})*[: e] = e)%, } e
  | m.id
  | μ(id: e) { (id: e)* }
  | ν(id: e) { (id: e)* }
  | let d* in e
  | e where d*
  | ...
d = [c] d
  | { d* }
  | id { d* }
  | id (id* | {id*} | (id*: e) | {id*: e})*[: e] = e
  | syntax nat%. ... = ...
  | open m