skylighting-core-0.7: test/expected/abc.agda.native

[ [ ( KeywordTok , "module" )
  , ( NormalTok , " Reals " )
  , ( KeywordTok , "where" )
  ]
, []
, [ ( NormalTok , "  " )
  , ( CommentTok , "-- (a set with properties of) the reals" )
  ]
, [ ( NormalTok , "  " )
  , ( KeywordTok , "data" )
  , ( NormalTok , " \8477 " )
  , ( OtherTok , ":" )
  , ( NormalTok , " " )
  , ( DataTypeTok , "Set" )
  , ( NormalTok , " " )
  , ( KeywordTok , "where" )
  ]
, [ ( NormalTok , "    r0 " )
  , ( OtherTok , ":" )
  , ( NormalTok , " \8477" )
  ]
, [ ( NormalTok , "    r1 " )
  , ( OtherTok , ":" )
  , ( NormalTok , " \8477" )
  ]
, [ ( NormalTok , "    " )
  , ( OtherTok , "_" )
  , ( NormalTok , "+" )
  , ( OtherTok , "_" )
  , ( NormalTok , " " )
  , ( OtherTok , ":" )
  , ( NormalTok , " \8477 " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " \8477 " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " \8477" )
  ]
, []
, [ ( NormalTok , "  " ) , ( CommentTok , "-- equality" ) ]
, [ ( NormalTok , "  " )
  , ( KeywordTok , "data" )
  , ( NormalTok , " " )
  , ( OtherTok , "_" )
  , ( NormalTok , "==" )
  , ( OtherTok , "_" )
  , ( NormalTok , " " )
  , ( OtherTok , ":" )
  , ( NormalTok , " \8477 " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " \8477 " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " " )
  , ( DataTypeTok , "Set" )
  , ( NormalTok , " " )
  , ( KeywordTok , "where" )
  ]
, [ ( NormalTok , "    AXrefl== " )
  , ( OtherTok , ":" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8704" )
  , ( NormalTok , " " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " r == r" )
  ]
, [ ( NormalTok , "    AXsymm== " )
  , ( OtherTok , ":" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8704" )
  , ( NormalTok , " " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r s" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " r == s " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " s == r" )
  ]
, [ ( NormalTok , "    AXtrans== " )
  , ( OtherTok , ":" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8704" )
  , ( NormalTok , " " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r s t" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " r == s " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " s == t " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " r == t" )
  ]
, [ ( NormalTok , "    AX+0 " )
  , ( OtherTok , ":" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8704" )
  , ( NormalTok , " " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " " )
  , ( OtherTok , "(" )
  , ( NormalTok , "r + r0" )
  , ( OtherTok , ")" )
  , ( NormalTok , " == r" )
  ]
, [ ( NormalTok , "    AXsymm+ " )
  , ( OtherTok , ":" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8704" )
  , ( NormalTok , " " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r s" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " " )
  , ( OtherTok , "(" )
  , ( NormalTok , "r + s" )
  , ( OtherTok , ")" )
  , ( NormalTok , " == " )
  , ( OtherTok , "(" )
  , ( NormalTok , "s + r" )
  , ( OtherTok , ")" )
  ]
, [ ( NormalTok , "    AX+== " )
  , ( OtherTok , ":" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8704" )
  , ( NormalTok , " " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r s t" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " r == s " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " " )
  , ( OtherTok , "(" )
  , ( NormalTok , "r + t" )
  , ( OtherTok , ")" )
  , ( NormalTok , " == " )
  , ( OtherTok , "(" )
  , ( NormalTok , "s + t" )
  , ( OtherTok , ")" )
  ]
, []
, [ ( NormalTok , "  THM0+ " )
  , ( OtherTok , ":" )
  , ( NormalTok , " " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r " )
  , ( OtherTok , ":" )
  , ( NormalTok , " \8477" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " r == " )
  , ( OtherTok , "(" )
  , ( NormalTok , "r0 + r" )
  , ( OtherTok , ")" )
  ]
, [ ( NormalTok , "  THM0+ " )
  , ( OtherTok , "=" )
  , ( NormalTok , " AXsymm== " )
  , ( OtherTok , "(" )
  , ( NormalTok , "AXtrans== AXsymm+ AX+0" )
  , ( OtherTok , ")" )
  ]
, [ ( NormalTok , "  " )
  , ( CommentTok
    , "-- AXsymm+ AX+0   r0 + r == r + r0 and r + r0 == r"
    )
  ]
, [ ( NormalTok , "  " )
  , ( CommentTok , "-- AXtrans==      so r0 + r == r" )
  ]
, [ ( NormalTok , "  " )
  , ( CommentTok , "-- AXsymm==       so r == r0 + r" )
  ]
, []
, [ ( NormalTok , "  THM0+alt " )
  , ( OtherTok , ":" )
  , ( NormalTok , " " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r " )
  , ( OtherTok , ":" )
  , ( NormalTok , " \8477" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " r == " )
  , ( OtherTok , "(" )
  , ( NormalTok , "r0 + r" )
  , ( OtherTok , ")" )
  ]
, [ ( NormalTok , "  THM0+alt " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "=" )
  , ( NormalTok , " AXsymm== " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r0 + r" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "((" )
  , ( NormalTok , "AXtrans== " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r0 + r" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r + r0" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r" )
  , ( OtherTok , "})" )
  , ( NormalTok , " " )
  , ( OtherTok , "(" )
  , ( NormalTok , "AXsymm+ " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r0" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r" )
  , ( OtherTok , "})" )
  , ( NormalTok , " " )
  , ( OtherTok , "(" )
  , ( NormalTok , "AX+0 " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r" )
  , ( OtherTok , "}))" )
  ]
, []
, [ ( NormalTok , "  " )
  , ( CommentTok , "-- strict partial ordering" )
  ]
, [ ( NormalTok , "  " )
  , ( KeywordTok , "data" )
  , ( NormalTok , " " )
  , ( OtherTok , "_" )
  , ( NormalTok , "<" )
  , ( OtherTok , "_" )
  , ( NormalTok , " " )
  , ( OtherTok , ":" )
  , ( NormalTok , " \8477 " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " \8477 " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " " )
  , ( DataTypeTok , "Set" )
  , ( NormalTok , " " )
  , ( KeywordTok , "where" )
  ]
, [ ( NormalTok , "    AXtrans<<< " )
  , ( OtherTok , ":" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8704" )
  , ( NormalTok , " " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r s t" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " r < s " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " s < t " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " r < t" )
  ]
, [ ( NormalTok , "    AX<=< " )
  , ( OtherTok , ":" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8704" )
  , ( NormalTok , " " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r s t" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " r < s " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " s == t " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " r < t" )
  ]
, [ ( NormalTok , "    AX=<< " )
  , ( OtherTok , ":" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8704" )
  , ( NormalTok , " " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r s t" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " r == s " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " s < t " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " r < t" )
  ]
, [ ( NormalTok , "    AX0<1 " )
  , ( OtherTok , ":" )
  , ( NormalTok , " r0 < r1" )
  ]
, [ ( NormalTok , "    AX+<< " )
  , ( OtherTok , ":" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8704" )
  , ( NormalTok , " " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r s t" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " r < s " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " " )
  , ( OtherTok , "(" )
  , ( NormalTok , "r + t" )
  , ( OtherTok , ")" )
  , ( NormalTok , " < " )
  , ( OtherTok , "(" )
  , ( NormalTok , "s + t" )
  , ( OtherTok , ")" )
  ]
, []
, [ ( NormalTok , "  THM<+1 " )
  , ( OtherTok , ":" )
  , ( NormalTok , " " )
  , ( OtherTok , "{" )
  , ( NormalTok , "r " )
  , ( OtherTok , ":" )
  , ( NormalTok , " \8477" )
  , ( OtherTok , "}" )
  , ( NormalTok , " " )
  , ( OtherTok , "\8594" )
  , ( NormalTok , " r < " )
  , ( OtherTok , "(" )
  , ( NormalTok , "r + r1" )
  , ( OtherTok , ")" )
  ]
, [ ( NormalTok , "  THM<+1 " )
  , ( OtherTok , "=" )
  , ( NormalTok , " AX<=< " )
  , ( OtherTok , "(" )
  , ( NormalTok , "AX=<< THM0+ " )
  , ( OtherTok , "(" )
  , ( NormalTok , "AX+<< AX0<1" )
  , ( OtherTok , "))" )
  , ( NormalTok , " AXsymm+" )
  ]
, [ ( NormalTok , "  " )
  , ( CommentTok , "-- AX0<1              0 < 1" )
  ]
, [ ( NormalTok , "  " )
  , ( CommentTok , "-- AX<+ %             so 0 + r < 1 + r" )
  ]
, [ ( NormalTok , "  " )
  , ( CommentTok , "-- AX=<< lem0+ %      so r < 1 + r" )
  ]
, [ ( NormalTok , "  " )
  , ( CommentTok , "-- AX<=< % AXsymm+    so r < r + 1" )
  ]
]