This is a literate Agda file. This span - span - will be linked to the record below:

record span : Set where
  constructor hey-look