
  0 | module Text.WebIDL.Types.Symbol
  1 | 
  2 | import Derive.Prelude
  3 | 
  4 | %default total
  5 | 
  6 | %language ElabReflection
  7 | 
  8 | ||| A single non-alphanumeric character that is not
  9 | ||| part of another recognized text token like a comment
 10 | ||| or floating point literal.
 11 | public export
 12 | data Symbol : Type where
 13 |   ||| An ellipsis : ...
 14 |   Ellipsis : Symbol
 15 | 
 16 |   ||| A single non-alphanumeric character like '=' or '{'.
 17 |   Symb     : (symb : Char) -> Symbol
 18 | 
 19 | %runElab derive "Symbol" [Eq,Show]
 20 | 
 21 | export %inline
 22 | Interpolation Symbol where
 23 |   interpolate Ellipsis = "..."
 24 |   interpolate (Symb c) = singleton c
 25 |