
  0 | module Core.Context.TTC
  1 | 
  2 | import Core.Binary
  3 | import Core.Context
  4 | 
  5 | %default covering
  6 | 
  7 | export
  8 | TTC BuiltinType where
  9 |     toBuf BuiltinNatural = tag 0
 10 |     toBuf NaturalToInteger = tag 1
 11 |     toBuf IntegerToNatural = tag 2
 12 |     fromBuf = case !getTag of
 13 |         0 => pure BuiltinNatural
 14 |         1 => pure NaturalToInteger
 15 |         2 => pure IntegerToNatural
 16 |         _ => corrupt "BuiltinType"
 17 |