@charset "UTF-8";
html {
  background: #fafafa;
  margin: 0;
  font-family: serif;
  font-size: 1.1em;
  color: #333;
  margin-bottom: 20%; }

.content {
  max-width: 40em;
  padding: 2em;
  margin: auto; }

a {
  color: #2C3E50;
  text-decoration-skip: ink;
  margin-bottom: -1px; }

h1 {
  font-weight: lighter; }

lighter {
  font-weight: lighter; }

h1, h2, h3, h4 {
  color: #111; }

h1 {
  font-size: 2rem;
  line-height: 3rem;
  margin-left: -2px; }

h2 {
  font-size: 1.5rem;
  line-height: 2rem;
  padding: 0;
  margin-left: -1px; }

h3 {
  margin: 0;
  padding-top: 1rem;
  line-height: 2rem;
  font-size: 1.1rem; }

hr {
  margin: 1em 0;
  padding: 0;
  border: 0;
  border-bottom: 1px solid #ddd; }

ul {
  list-style: none;
  margin: 0;
  padding: 0; }

li {
  padding-bottom: .5rem;
  text-indent: -0.7em; }

li:before {
  content: "■ ";
  color: #919191; }

.extra {
  font-size: 80%;
  color: #444;
  border-top: 1px solid #f2f2f2;
  padding-top: .2em;
  margin-top: .2em;
  padding-bottom: 1em; }

ul.extra li, ul.extra {
  line-height: 1.1rem !important;
  text-indent: 0; }

abbr {
  font-variant-caps: all-small-caps;
  font-feature-settings: "c2sc", "smcp"; }

ul.inline li {
  display: inline;
  text-indent: 0.7em !important; }
ul.inline li:before {
  content: ''; }
ul.inline li + li:before {
  content: '\25AA ';
  color: #919191;
  padding: 0 .3em 0 .1em; }

.pseudo {
  white-space: pre-wrap;
  font-size: 16px;
  font-weight: normal;
  font-family: gentium,serif;
  line-height: 120%; }
  .pseudo .op, .pseudo .function, .pseudo .number {
    font-style: normal; }
  .pseudo .op {
    padding: 0 1px; }
  .pseudo .symbol {
    text-transform: lowercase;
    font-weight: bold;
    font-style: normal;
    font-family: sans-serif;
    font-size: 14px; }
  .pseudo .function {
    font-style: normal;
    font-family: sans-serif;
    font-size: 14px; }
  .pseudo .string {
    font-family: monospace;
    font-size: 14px; }
  .pseudo .comment {
    white-space: normal;
    font-style: italic;
    font-size: 95%;
    color: #2b2b2b; }
  .pseudo .indent {
    font-family: monospace; }

@media print {
  html {
    font-size: 8pt;
    color: #000;
    background: #fff; }

  @page {
    margin: 0;
    height: 9.5in; }
  body {
    margin: 0cm; } }