@font-face { font-family: KaTeX_AMS; src: url(fonts/KaTeX_AMS-Regular.eot); src: url(fonts/KaTeX_AMS-Regular.eot#iefix) format("embedded-opentype"), url(fonts/KaTeX_AMS-Regular.woff2) format("woff2"), url(fonts/KaTeX_AMS-Regular.woff) format("woff"), url(fonts/KaTeX_AMS-Regular.ttf) format("ttf"); font-weight: 400; font-style: normal; }
@font-face { font-family: KaTeX_Caligraphic; src: url(fonts/KaTeX_Caligraphic-Bold.eot); src: url(fonts/KaTeX_Caligraphic-Bold.eot#iefix) format("embedded-opentype"), url(fonts/KaTeX_Caligraphic-Bold.woff2) format("woff2"), url(fonts/KaTeX_Caligraphic-Bold.woff) format("woff"), url(fonts/KaTeX_Caligraphic-Bold.ttf) format("ttf"); font-weight: 700; font-style: normal; }
@font-face { font-family: KaTeX_Caligraphic; src: url(fonts/KaTeX_Caligraphic-Regular.eot); src: url(fonts/KaTeX_Caligraphic-Regular.eot#iefix) format("embedded-opentype"), url(fonts/KaTeX_Caligraphic-Regular.woff2) format("woff2"), url(fonts/KaTeX_Caligraphic-Regular.woff) format("woff"), url(fonts/KaTeX_Caligraphic-Regular.ttf) format("ttf"); font-weight: 400; font-style: normal; }
@font-face { font-family: KaTeX_Fraktur; src: url(fonts/KaTeX_Fraktur-Bold.eot); src: url(fonts/KaTeX_Fraktur-Bold.eot#iefix) format("embedded-opentype"), url(fonts/KaTeX_Fraktur-Bold.woff2) format("woff2"), url(fonts/KaTeX_Fraktur-Bold.woff) format("woff"), url(fonts/KaTeX_Fraktur-Bold.ttf) format("ttf"); font-weight: 700; font-style: normal; }
@font-face { font-family: KaTeX_Fraktur; src: url(fonts/KaTeX_Fraktur-Regular.eot); src: url(fonts/KaTeX_Fraktur-Regular.eot#iefix) format("embedded-opentype"), url(fonts/KaTeX_Fraktur-Regular.woff2) format("woff2"), url(fonts/KaTeX_Fraktur-Regular.woff) format("woff"), url(fonts/KaTeX_Fraktur-Regular.ttf) format("ttf"); font-weight: 400; font-style: normal; }
@font-face { font-family: KaTeX_Main; src: url(fonts/KaTeX_Main-Bold.eot); src: url(fonts/KaTeX_Main-Bold.eot#iefix) format("embedded-opentype"), url(fonts/KaTeX_Main-Bold.woff2) format("woff2"), url(fonts/KaTeX_Main-Bold.woff) format("woff"), url(fonts/KaTeX_Main-Bold.ttf) format("ttf"); font-weight: 700; font-style: normal; }
@font-face { font-family: KaTeX_Main; src: url(fonts/KaTeX_Main-Italic.eot); src: url(fonts/KaTeX_Main-Italic.eot#iefix) format("embedded-opentype"), url(fonts/KaTeX_Main-Italic.woff2) format("woff2"), url(fonts/KaTeX_Main-Italic.woff) format("woff"), url(fonts/KaTeX_Main-Italic.ttf) format("ttf"); font-weight: 400; font-style: italic; }
@font-face { font-family: KaTeX_Main; src: url(fonts/KaTeX_Main-Regular.eot); src: url(fonts/KaTeX_Main-Regular.eot#iefix) format("embedded-opentype"), url(fonts/KaTeX_Main-Regular.woff2) format("woff2"), url(fonts/KaTeX_Main-Regular.woff) format("woff"), url(fonts/KaTeX_Main-Regular.ttf) format("ttf"); font-weight: 400; font-style: normal; }
@font-face { font-family: KaTeX_Math; src: url(fonts/KaTeX_Math-Italic.eot); src: url(fonts/KaTeX_Math-Italic.eot#iefix) format("embedded-opentype"), url(fonts/KaTeX_Math-Italic.woff2) format("woff2"), url(fonts/KaTeX_Math-Italic.woff) format("woff"), url(fonts/KaTeX_Math-Italic.ttf) format("ttf"); font-weight: 400; font-style: italic; }
@font-face { font-family: KaTeX_SansSerif; src: url(fonts/KaTeX_SansSerif-Regular.eot); src: url(fonts/KaTeX_SansSerif-Regular.eot#iefix) format("embedded-opentype"), url(fonts/KaTeX_SansSerif-Regular.woff2) format("woff2"), url(fonts/KaTeX_SansSerif-Regular.woff) format("woff"), url(fonts/KaTeX_SansSerif-Regular.ttf) format("ttf"); font-weight: 400; font-style: normal; }
@font-face { font-family: KaTeX_Script; src: url(fonts/KaTeX_Script-Regular.eot); src: url(fonts/KaTeX_Script-Regular.eot#iefix) format("embedded-opentype"), url(fonts/KaTeX_Script-Regular.woff2) format("woff2"), url(fonts/KaTeX_Script-Regular.woff) format("woff"), url(fonts/KaTeX_Script-Regular.ttf) format("ttf"); font-weight: 400; font-style: normal; }
@font-face { font-family: KaTeX_Size1; src: url(fonts/KaTeX_Size1-Regular.eot); src: url(fonts/KaTeX_Size1-Regular.eot#iefix) format("embedded-opentype"), url(fonts/KaTeX_Size1-Regular.woff2) format("woff2"), url(fonts/KaTeX_Size1-Regular.woff) format("woff"), url(fonts/KaTeX_Size1-Regular.ttf) format("ttf"); font-weight: 400; font-style: normal; }
@font-face { font-family: KaTeX_Size2; src: url(fonts/KaTeX_Size2-Regular.eot); src: url(fonts/KaTeX_Size2-Regular.eot#iefix) format("embedded-opentype"), url(fonts/KaTeX_Size2-Regular.woff2) format("woff2"), url(fonts/KaTeX_Size2-Regular.woff) format("woff"), url(fonts/KaTeX_Size2-Regular.ttf) format("ttf"); font-weight: 400; font-style: normal; }
@font-face { font-family: KaTeX_Size3; src: url(fonts/KaTeX_Size3-Regular.eot); src: url(fonts/KaTeX_Size3-Regular.eot#iefix) format("embedded-opentype"), url(fonts/KaTeX_Size3-Regular.woff2) format("woff2"), url(fonts/KaTeX_Size3-Regular.woff) format("woff"), url(fonts/KaTeX_Size3-Regular.ttf) format("ttf"); font-weight: 400; font-style: normal; }
@font-face { font-family: KaTeX_Size4; src: url(fonts/KaTeX_Size4-Regular.eot); src: url(fonts/KaTeX_Size4-Regular.eot#iefix) format("embedded-opentype"), url(fonts/KaTeX_Size4-Regular.woff2) format("woff2"), url(fonts/KaTeX_Size4-Regular.woff) format("woff"), url(fonts/KaTeX_Size4-Regular.ttf) format("ttf"); font-weight: 400; font-style: normal; }
@font-face { font-family: KaTeX_Typewriter; src: url(fonts/KaTeX_Typewriter-Regular.eot); src: url(fonts/KaTeX_Typewriter-Regular.eot#iefix) format("embedded-opentype"), url(fonts/KaTeX_Typewriter-Regular.woff2) format("woff2"), url(fonts/KaTeX_Typewriter-Regular.woff) format("woff"), url(fonts/KaTeX_Typewriter-Regular.ttf) format("ttf"); font-weight: 400; font-style: normal; }
.katex-display { display: block; margin: 1em 0; text-align: center; }

.katex-display > .katex { display: inline-block; text-align: initial; }

.katex { font: 400 1.21em KaTeX_Main; line-height: 1.2; white-space: nowrap; text-indent: 0; }

.katex .katex-html { display: inline-block; }

.katex .katex-mathml { position: absolute; clip: rect(1px, 1px, 1px, 1px); padding: 0; border: 0; height: 1px; width: 1px; overflow: hidden; }

.katex .base, .katex .strut { display: inline-block; }

.katex .mathit { font-family: KaTeX_Math; font-style: italic; }

.katex .mathbf { font-family: KaTeX_Main; font-weight: 700; }

.katex .amsrm, .katex .mathbb { font-family: KaTeX_AMS; }

.katex .mathcal { font-family: KaTeX_Caligraphic; }

.katex .mathfrak { font-family: KaTeX_Fraktur; }

.katex .mathtt { font-family: KaTeX_Typewriter; }

.katex .mathscr { font-family: KaTeX_Script; }

.katex .mathsf { font-family: KaTeX_SansSerif; }

.katex .mainit { font-family: KaTeX_Main; font-style: italic; }

.katex .textstyle > .mord + .mop { margin-left: .16667em; }

.katex .textstyle > .mord + .mbin { margin-left: .22222em; }

.katex .textstyle > .mord + .mrel { margin-left: .27778em; }

.katex .textstyle > .mop + .mop, .katex .textstyle > .mop + .mord, .katex .textstyle > .mord + .minner { margin-left: .16667em; }

.katex .textstyle > .mop + .mrel { margin-left: .27778em; }

.katex .textstyle > .mop + .minner { margin-left: .16667em; }

.katex .textstyle > .mbin + .minner, .katex .textstyle > .mbin + .mop, .katex .textstyle > .mbin + .mopen, .katex .textstyle > .mbin + .mord { margin-left: .22222em; }

.katex .textstyle > .mrel + .minner, .katex .textstyle > .mrel + .mop, .katex .textstyle > .mrel + .mopen, .katex .textstyle > .mrel + .mord { margin-left: .27778em; }

.katex .textstyle > .mclose + .mop { margin-left: .16667em; }

.katex .textstyle > .mclose + .mbin { margin-left: .22222em; }

.katex .textstyle > .mclose + .mrel { margin-left: .27778em; }

.katex .textstyle > .mclose + .minner, .katex .textstyle > .minner + .mop, .katex .textstyle > .minner + .mord, .katex .textstyle > .mpunct + .mclose, .katex .textstyle > .mpunct + .minner, .katex .textstyle > .mpunct + .mop, .katex .textstyle > .mpunct + .mopen, .katex .textstyle > .mpunct + .mord, .katex .textstyle > .mpunct + .mpunct, .katex .textstyle > .mpunct + .mrel { margin-left: .16667em; }

.katex .textstyle > .minner + .mbin { margin-left: .22222em; }

.katex .textstyle > .minner + .mrel { margin-left: .27778em; }

.katex .mclose + .mop, .katex .minner + .mop, .katex .mop + .mop, .katex .mop + .mord, .katex .mord + .mop, .katex .textstyle > .minner + .minner, .katex .textstyle > .minner + .mopen, .katex .textstyle > .minner + .mpunct { margin-left: .16667em; }

.katex .reset-textstyle.textstyle { font-size: 1em; }

.katex .reset-textstyle.scriptstyle { font-size: .7em; }

.katex .reset-textstyle.scriptscriptstyle { font-size: .5em; }

.katex .reset-scriptstyle.textstyle { font-size: 1.42857em; }

.katex .reset-scriptstyle.scriptstyle { font-size: 1em; }

.katex .reset-scriptstyle.scriptscriptstyle { font-size: .71429em; }

.katex .reset-scriptscriptstyle.textstyle { font-size: 2em; }

.katex .reset-scriptscriptstyle.scriptstyle { font-size: 1.4em; }

.katex .reset-scriptscriptstyle.scriptscriptstyle { font-size: 1em; }

.katex .style-wrap { position: relative; }

.katex .vlist { display: inline-block; }

.katex .vlist > span { display: block; height: 0; position: relative; }

.katex .vlist > span > span { display: inline-block; }

.katex .vlist .baseline-fix { display: inline-table; table-layout: fixed; }

.katex .msupsub { text-align: left; }

.katex .mfrac > span > span { text-align: center; }

.katex .mfrac .frac-line { width: 100%; }

.katex .mfrac .frac-line:before { border-bottom-style: solid; border-bottom-width: 1px; content: ""; display: block; }

.katex .mfrac .frac-line:after { border-bottom-style: solid; border-bottom-width: .04em; content: ""; display: block; margin-top: -1px; }

.katex .mspace { display: inline-block; }

.katex .mspace.negativethinspace { margin-left: -.16667em; }

.katex .mspace.thinspace { width: .16667em; }

.katex .mspace.mediumspace { width: .22222em; }

.katex .mspace.thickspace { width: .27778em; }

.katex .mspace.enspace { width: .5em; }

.katex .mspace.quad { width: 1em; }

.katex .mspace.qquad { width: 2em; }

.katex .llap, .katex .rlap { width: 0; position: relative; }

.katex .llap > .inner, .katex .rlap > .inner { position: absolute; }

.katex .llap > .fix, .katex .rlap > .fix { display: inline-block; }

.katex .llap > .inner { right: 0; }

.katex .rlap > .inner { left: 0; }

.katex .katex-logo .a { font-size: .75em; margin-left: -.32em; position: relative; top: -.2em; }

.katex .katex-logo .t { margin-left: -.23em; }

.katex .katex-logo .e { margin-left: -.1667em; position: relative; top: .2155em; }

.katex .katex-logo .x { margin-left: -.125em; }

.katex .rule { display: inline-block; border: 0 solid; position: relative; }

.katex .overline .overline-line, .katex .underline .underline-line { width: 100%; }

.katex .overline .overline-line:before, .katex .underline .underline-line:before { border-bottom-style: solid; border-bottom-width: 1px; content: ""; display: block; }

.katex .overline .overline-line:after, .katex .underline .underline-line:after { border-bottom-style: solid; border-bottom-width: .04em; content: ""; display: block; margin-top: -1px; }

.katex .sqrt > .sqrt-sign { position: relative; }

.katex .sqrt .sqrt-line { width: 100%; }

.katex .sqrt .sqrt-line:before { border-bottom-style: solid; border-bottom-width: 1px; content: ""; display: block; }

.katex .sqrt .sqrt-line:after { border-bottom-style: solid; border-bottom-width: .04em; content: ""; display: block; margin-top: -1px; }

.katex .sqrt > .root { margin-left: .27777778em; margin-right: -.55555556em; }

.katex .fontsize-ensurer, .katex .sizing { display: inline-block; }

.katex .fontsize-ensurer.reset-size1.size1, .katex .sizing.reset-size1.size1 { font-size: 1em; }

.katex .fontsize-ensurer.reset-size1.size2, .katex .sizing.reset-size1.size2 { font-size: 1.4em; }

.katex .fontsize-ensurer.reset-size1.size3, .katex .sizing.reset-size1.size3 { font-size: 1.6em; }

.katex .fontsize-ensurer.reset-size1.size4, .katex .sizing.reset-size1.size4 { font-size: 1.8em; }

.katex .fontsize-ensurer.reset-size1.size5, .katex .sizing.reset-size1.size5 { font-size: 2em; }

.katex .fontsize-ensurer.reset-size1.size6, .katex .sizing.reset-size1.size6 { font-size: 2.4em; }

.katex .fontsize-ensurer.reset-size1.size7, .katex .sizing.reset-size1.size7 { font-size: 2.88em; }

.katex .fontsize-ensurer.reset-size1.size8, .katex .sizing.reset-size1.size8 { font-size: 3.46em; }

.katex .fontsize-ensurer.reset-size1.size9, .katex .sizing.reset-size1.size9 { font-size: 4.14em; }

.katex .fontsize-ensurer.reset-size1.size10, .katex .sizing.reset-size1.size10 { font-size: 4.98em; }

.katex .fontsize-ensurer.reset-size2.size1, .katex .sizing.reset-size2.size1 { font-size: .71428571em; }

.katex .fontsize-ensurer.reset-size2.size2, .katex .sizing.reset-size2.size2 { font-size: 1em; }

.katex .fontsize-ensurer.reset-size2.size3, .katex .sizing.reset-size2.size3 { font-size: 1.14285714em; }

.katex .fontsize-ensurer.reset-size2.size4, .katex .sizing.reset-size2.size4 { font-size: 1.28571429em; }

.katex .fontsize-ensurer.reset-size2.size5, .katex .sizing.reset-size2.size5 { font-size: 1.42857143em; }

.katex .fontsize-ensurer.reset-size2.size6, .katex .sizing.reset-size2.size6 { font-size: 1.71428571em; }

.katex .fontsize-ensurer.reset-size2.size7, .katex .sizing.reset-size2.size7 { font-size: 2.05714286em; }

.katex .fontsize-ensurer.reset-size2.size8, .katex .sizing.reset-size2.size8 { font-size: 2.47142857em; }

.katex .fontsize-ensurer.reset-size2.size9, .katex .sizing.reset-size2.size9 { font-size: 2.95714286em; }

.katex .fontsize-ensurer.reset-size2.size10, .katex .sizing.reset-size2.size10 { font-size: 3.55714286em; }

.katex .fontsize-ensurer.reset-size3.size1, .katex .sizing.reset-size3.size1 { font-size: .625em; }

.katex .fontsize-ensurer.reset-size3.size2, .katex .sizing.reset-size3.size2 { font-size: .875em; }

.katex .fontsize-ensurer.reset-size3.size3, .katex .sizing.reset-size3.size3 { font-size: 1em; }

.katex .fontsize-ensurer.reset-size3.size4, .katex .sizing.reset-size3.size4 { font-size: 1.125em; }

.katex .fontsize-ensurer.reset-size3.size5, .katex .sizing.reset-size3.size5 { font-size: 1.25em; }

.katex .fontsize-ensurer.reset-size3.size6, .katex .sizing.reset-size3.size6 { font-size: 1.5em; }

.katex .fontsize-ensurer.reset-size3.size7, .katex .sizing.reset-size3.size7 { font-size: 1.8em; }

.katex .fontsize-ensurer.reset-size3.size8, .katex .sizing.reset-size3.size8 { font-size: 2.1625em; }

.katex .fontsize-ensurer.reset-size3.size9, .katex .sizing.reset-size3.size9 { font-size: 2.5875em; }

.katex .fontsize-ensurer.reset-size3.size10, .katex .sizing.reset-size3.size10 { font-size: 3.1125em; }

.katex .fontsize-ensurer.reset-size4.size1, .katex .sizing.reset-size4.size1 { font-size: .55555556em; }

.katex .fontsize-ensurer.reset-size4.size2, .katex .sizing.reset-size4.size2 { font-size: .77777778em; }

.katex .fontsize-ensurer.reset-size4.size3, .katex .sizing.reset-size4.size3 { font-size: .88888889em; }

.katex .fontsize-ensurer.reset-size4.size4, .katex .sizing.reset-size4.size4 { font-size: 1em; }

.katex .fontsize-ensurer.reset-size4.size5, .katex .sizing.reset-size4.size5 { font-size: 1.11111111em; }

.katex .fontsize-ensurer.reset-size4.size6, .katex .sizing.reset-size4.size6 { font-size: 1.33333333em; }

.katex .fontsize-ensurer.reset-size4.size7, .katex .sizing.reset-size4.size7 { font-size: 1.6em; }

.katex .fontsize-ensurer.reset-size4.size8, .katex .sizing.reset-size4.size8 { font-size: 1.92222222em; }

.katex .fontsize-ensurer.reset-size4.size9, .katex .sizing.reset-size4.size9 { font-size: 2.3em; }

.katex .fontsize-ensurer.reset-size4.size10, .katex .sizing.reset-size4.size10 { font-size: 2.76666667em; }

.katex .fontsize-ensurer.reset-size5.size1, .katex .sizing.reset-size5.size1 { font-size: .5em; }

.katex .fontsize-ensurer.reset-size5.size2, .katex .sizing.reset-size5.size2 { font-size: .7em; }

.katex .fontsize-ensurer.reset-size5.size3, .katex .sizing.reset-size5.size3 { font-size: .8em; }

.katex .fontsize-ensurer.reset-size5.size4, .katex .sizing.reset-size5.size4 { font-size: .9em; }

.katex .fontsize-ensurer.reset-size5.size5, .katex .sizing.reset-size5.size5 { font-size: 1em; }

.katex .fontsize-ensurer.reset-size5.size6, .katex .sizing.reset-size5.size6 { font-size: 1.2em; }

.katex .fontsize-ensurer.reset-size5.size7, .katex .sizing.reset-size5.size7 { font-size: 1.44em; }

.katex .fontsize-ensurer.reset-size5.size8, .katex .sizing.reset-size5.size8 { font-size: 1.73em; }

.katex .fontsize-ensurer.reset-size5.size9, .katex .sizing.reset-size5.size9 { font-size: 2.07em; }

.katex .fontsize-ensurer.reset-size5.size10, .katex .sizing.reset-size5.size10 { font-size: 2.49em; }

.katex .fontsize-ensurer.reset-size6.size1, .katex .sizing.reset-size6.size1 { font-size: .41666667em; }

.katex .fontsize-ensurer.reset-size6.size2, .katex .sizing.reset-size6.size2 { font-size: .58333333em; }

.katex .fontsize-ensurer.reset-size6.size3, .katex .sizing.reset-size6.size3 { font-size: .66666667em; }

.katex .fontsize-ensurer.reset-size6.size4, .katex .sizing.reset-size6.size4 { font-size: .75em; }

.katex .fontsize-ensurer.reset-size6.size5, .katex .sizing.reset-size6.size5 { font-size: .83333333em; }

.katex .fontsize-ensurer.reset-size6.size6, .katex .sizing.reset-size6.size6 { font-size: 1em; }

.katex .fontsize-ensurer.reset-size6.size7, .katex .sizing.reset-size6.size7 { font-size: 1.2em; }

.katex .fontsize-ensurer.reset-size6.size8, .katex .sizing.reset-size6.size8 { font-size: 1.44166667em; }

.katex .fontsize-ensurer.reset-size6.size9, .katex .sizing.reset-size6.size9 { font-size: 1.725em; }

.katex .fontsize-ensurer.reset-size6.size10, .katex .sizing.reset-size6.size10 { font-size: 2.075em; }

.katex .fontsize-ensurer.reset-size7.size1, .katex .sizing.reset-size7.size1 { font-size: .34722222em; }

.katex .fontsize-ensurer.reset-size7.size2, .katex .sizing.reset-size7.size2 { font-size: .48611111em; }

.katex .fontsize-ensurer.reset-size7.size3, .katex .sizing.reset-size7.size3 { font-size: .55555556em; }

.katex .fontsize-ensurer.reset-size7.size4, .katex .sizing.reset-size7.size4 { font-size: .625em; }

.katex .fontsize-ensurer.reset-size7.size5, .katex .sizing.reset-size7.size5 { font-size: .69444444em; }

.katex .fontsize-ensurer.reset-size7.size6, .katex .sizing.reset-size7.size6 { font-size: .83333333em; }

.katex .fontsize-ensurer.reset-size7.size7, .katex .sizing.reset-size7.size7 { font-size: 1em; }

.katex .fontsize-ensurer.reset-size7.size8, .katex .sizing.reset-size7.size8 { font-size: 1.20138889em; }

.katex .fontsize-ensurer.reset-size7.size9, .katex .sizing.reset-size7.size9 { font-size: 1.4375em; }

.katex .fontsize-ensurer.reset-size7.size10, .katex .sizing.reset-size7.size10 { font-size: 1.72916667em; }

.katex .fontsize-ensurer.reset-size8.size1, .katex .sizing.reset-size8.size1 { font-size: .28901734em; }

.katex .fontsize-ensurer.reset-size8.size2, .katex .sizing.reset-size8.size2 { font-size: .40462428em; }

.katex .fontsize-ensurer.reset-size8.size3, .katex .sizing.reset-size8.size3 { font-size: .46242775em; }

.katex .fontsize-ensurer.reset-size8.size4, .katex .sizing.reset-size8.size4 { font-size: .52023121em; }

.katex .fontsize-ensurer.reset-size8.size5, .katex .sizing.reset-size8.size5 { font-size: .57803468em; }

.katex .fontsize-ensurer.reset-size8.size6, .katex .sizing.reset-size8.size6 { font-size: .69364162em; }

.katex .fontsize-ensurer.reset-size8.size7, .katex .sizing.reset-size8.size7 { font-size: .83236994em; }

.katex .fontsize-ensurer.reset-size8.size8, .katex .sizing.reset-size8.size8 { font-size: 1em; }

.katex .fontsize-ensurer.reset-size8.size9, .katex .sizing.reset-size8.size9 { font-size: 1.19653179em; }

.katex .fontsize-ensurer.reset-size8.size10, .katex .sizing.reset-size8.size10 { font-size: 1.43930636em; }

.katex .fontsize-ensurer.reset-size9.size1, .katex .sizing.reset-size9.size1 { font-size: .24154589em; }

.katex .fontsize-ensurer.reset-size9.size2, .katex .sizing.reset-size9.size2 { font-size: .33816425em; }

.katex .fontsize-ensurer.reset-size9.size3, .katex .sizing.reset-size9.size3 { font-size: .38647343em; }

.katex .fontsize-ensurer.reset-size9.size4, .katex .sizing.reset-size9.size4 { font-size: .43478261em; }

.katex .fontsize-ensurer.reset-size9.size5, .katex .sizing.reset-size9.size5 { font-size: .48309179em; }

.katex .fontsize-ensurer.reset-size9.size6, .katex .sizing.reset-size9.size6 { font-size: .57971014em; }

.katex .fontsize-ensurer.reset-size9.size7, .katex .sizing.reset-size9.size7 { font-size: .69565217em; }

.katex .fontsize-ensurer.reset-size9.size8, .katex .sizing.reset-size9.size8 { font-size: .83574879em; }

.katex .fontsize-ensurer.reset-size9.size9, .katex .sizing.reset-size9.size9 { font-size: 1em; }

.katex .fontsize-ensurer.reset-size9.size10, .katex .sizing.reset-size9.size10 { font-size: 1.20289855em; }

.katex .fontsize-ensurer.reset-size10.size1, .katex .sizing.reset-size10.size1 { font-size: .20080321em; }

.katex .fontsize-ensurer.reset-size10.size2, .katex .sizing.reset-size10.size2 { font-size: .2811245em; }

.katex .fontsize-ensurer.reset-size10.size3, .katex .sizing.reset-size10.size3 { font-size: .32128514em; }

.katex .fontsize-ensurer.reset-size10.size4, .katex .sizing.reset-size10.size4 { font-size: .36144578em; }

.katex .fontsize-ensurer.reset-size10.size5, .katex .sizing.reset-size10.size5 { font-size: .40160643em; }

.katex .fontsize-ensurer.reset-size10.size6, .katex .sizing.reset-size10.size6 { font-size: .48192771em; }

.katex .fontsize-ensurer.reset-size10.size7, .katex .sizing.reset-size10.size7 { font-size: .57831325em; }

.katex .fontsize-ensurer.reset-size10.size8, .katex .sizing.reset-size10.size8 { font-size: .69477912em; }

.katex .fontsize-ensurer.reset-size10.size9, .katex .sizing.reset-size10.size9 { font-size: .8313253em; }

.katex .fontsize-ensurer.reset-size10.size10, .katex .sizing.reset-size10.size10 { font-size: 1em; }

.katex .delimsizing.size1 { font-family: KaTeX_Size1; }

.katex .delimsizing.size2 { font-family: KaTeX_Size2; }

.katex .delimsizing.size3 { font-family: KaTeX_Size3; }

.katex .delimsizing.size4 { font-family: KaTeX_Size4; }

.katex .delimsizing.mult .delim-size1 > span { font-family: KaTeX_Size1; }

.katex .delimsizing.mult .delim-size4 > span { font-family: KaTeX_Size4; }

.katex .nulldelimiter { display: inline-block; width: .12em; }

.katex .op-symbol { position: relative; }

.katex .op-symbol.small-op { font-family: KaTeX_Size1; }

.katex .op-symbol.large-op { font-family: KaTeX_Size2; }

.katex .accent > .vlist > span, .katex .op-limits > .vlist > span { text-align: center; }

.katex .accent .accent-body > span { width: 0; }

.katex .accent .accent-body.accent-vec > span { position: relative; left: .326em; }

.katex .mtable .vertical-separator { display: inline-block; margin: 0 -.025em; border-right: .05em solid #000; }

.katex .mtable .arraycolsep { display: inline-block; }

.katex .mtable .col-align-c > .vlist { text-align: center; }

.katex .mtable .col-align-l > .vlist { text-align: left; }

.katex .mtable .col-align-r > .vlist { text-align: right; }

/** Reset some basic elements */
body, h1, h2, h3, h4, h5, h6, p, blockquote, pre, hr, dl, dd, ol, ul, figure { margin: 0; padding: 0; }

/** Basic styling */
body { font: 400 16px/1.5 -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto, Helvetica, Arial, sans-serif, "Apple Color Emoji", "Segoe UI Emoji", "Segoe UI Symbol"; color: #111; background-color: #fdfdfd; -webkit-text-size-adjust: 100%; -webkit-font-feature-settings: "kern" 1; -moz-font-feature-settings: "kern" 1; -o-font-feature-settings: "kern" 1; font-feature-settings: "kern" 1; font-kerning: normal; display: flex; min-height: 100vh; flex-direction: column; }

/** Set `margin-bottom` to maintain vertical rhythm */
h1, h2, h3, h4, h5, h6, p, blockquote, pre, ul, ol, dl, figure, .highlight { margin-bottom: 15px; }

/** `main` element */
main { display: block; /* Default value of `display` of `main` element is 'inline' in IE 11. */ }

/** Images */
img { max-width: 100%; vertical-align: middle; }

/** Figures */
figure > img { display: block; }

figcaption { font-size: 14px; }

/** Lists */
ul, ol { margin-left: 30px; }

li > ul, li > ol { margin-bottom: 0; }

/** Headings */
h1, h2, h3, h4, h5, h6 { font-weight: 400; }

/** Links */
a { color: #2a7ae2; text-decoration: none; }
a:visited { color: #1756a9; }
a:hover { color: #111; text-decoration: underline; }
.social-media-list a:hover { text-decoration: none; }
.social-media-list a:hover .username { text-decoration: underline; }

/** Blockquotes */
blockquote { color: #828282; border-left: 4px solid #e8e8e8; padding-left: 15px; font-size: 18px; letter-spacing: -1px; font-style: italic; }
blockquote > :last-child { margin-bottom: 0; }

/** Code formatting */
pre, code { font-size: 15px; border: 1px solid #e8e8e8; border-radius: 3px; background-color: #eef; }

code { padding: 1px 5px; }

pre { padding: 8px 12px; overflow-x: auto; }
pre > code { border: 0; padding-right: 0; padding-left: 0; }

/** Wrapper */
.wrapper { max-width: -webkit-calc(800px - (30px * 2)); max-width: calc(800px - (30px * 2)); margin-right: auto; margin-left: auto; padding-right: 30px; padding-left: 30px; }
@media screen and (max-width: 800px) { .wrapper { max-width: -webkit-calc(800px - (30px)); max-width: calc(800px - (30px)); padding-right: 15px; padding-left: 15px; } }

/** Clearfix */
.wrapper:after, .footer-col-wrapper:after { content: ""; display: table; clear: both; }

/** Icons */
.svg-icon { width: 16px; height: 16px; display: inline-block; fill: #828282; padding-right: 5px; vertical-align: text-top; }

.social-media-list li + li { padding-top: 5px; }

/** Tables */
table { margin-bottom: 30px; width: 100%; text-align: left; color: #3f3f3f; border-collapse: collapse; border: 1px solid #e8e8e8; }
table tr:nth-child(even) { background-color: #f7f7f7; }
table th, table td { padding: 10px 15px; }
table th { background-color: #f0f0f0; border: 1px solid #dedede; border-bottom-color: #c9c9c9; }
table td { border: 1px solid #e8e8e8; }

/** Site header */
.site-header { border-top: 5px solid #424242; border-bottom: 1px solid #e8e8e8; min-height: 55.95px; position: relative; }

.site-title { font-size: 26px; font-weight: 300; line-height: 54px; letter-spacing: -1px; margin-bottom: 0; float: left; }
.site-title, .site-title:visited { color: #424242; }

.site-nav { float: right; line-height: 54px; }
.site-nav .nav-trigger { display: none; }
.site-nav .menu-icon { display: none; }
.site-nav .page-link { color: #111; line-height: 1.5; }
.site-nav .page-link:not(:last-child) { margin-right: 20px; }
@media screen and (max-width: 600px) { .site-nav { position: absolute; top: 9px; right: 15px; background-color: #fdfdfd; border: 1px solid #e8e8e8; border-radius: 5px; text-align: right; }
  .site-nav label[for="nav-trigger"] { display: block; float: right; width: 36px; height: 36px; z-index: 2; cursor: pointer; }
  .site-nav .menu-icon { display: block; float: right; width: 36px; height: 26px; line-height: 0; padding-top: 10px; text-align: center; }
  .site-nav .menu-icon > svg { fill: #424242; }
  .site-nav input ~ .trigger { clear: both; display: none; }
  .site-nav input:checked ~ .trigger { display: block; padding-bottom: 5px; }
  .site-nav .page-link { display: block; padding: 5px 10px; margin-left: 20px; }
  .site-nav .page-link:not(:last-child) { margin-right: 0; } }

/** Site footer */
.site-footer { border-top: 1px solid #e8e8e8; padding: 30px 0; }

.footer-heading { font-size: 18px; margin-bottom: 15px; }

.contact-list, .social-media-list { list-style: none; margin-left: 0; }

.footer-col-wrapper { font-size: 15px; color: #828282; margin-left: -15px; }

.footer-col { float: left; margin-bottom: 15px; padding-left: 15px; }

.footer-col-1 { width: -webkit-calc(35% - (30px / 2)); width: calc(35% - (30px / 2)); }

.footer-col-2 { width: -webkit-calc(20% - (30px / 2)); width: calc(20% - (30px / 2)); }

.footer-col-3 { width: -webkit-calc(45% - (30px / 2)); width: calc(45% - (30px / 2)); }

@media screen and (max-width: 800px) { .footer-col-1, .footer-col-2 { width: -webkit-calc(50% - (30px / 2)); width: calc(50% - (30px / 2)); }
  .footer-col-3 { width: -webkit-calc(100% - (30px / 2)); width: calc(100% - (30px / 2)); } }
@media screen and (max-width: 600px) { .footer-col { float: none; width: -webkit-calc(100% - (30px / 2)); width: calc(100% - (30px / 2)); } }
/** Page content */
.page-content { padding: 30px 0; flex: 1; }

.page-heading { font-size: 32px; }

.post-list-heading { font-size: 28px; }

.post-list { margin-left: 0; list-style: none; }
.post-list > li { margin-bottom: 30px; }

.post-meta { font-size: 14px; color: #828282; }

.post-link { display: block; font-size: 24px; }

/** Posts */
.post-header { margin-bottom: 30px; }

.post-title { font-size: 42px; letter-spacing: -1px; line-height: 1; }
@media screen and (max-width: 800px) { .post-title { font-size: 36px; } }

.post-content { margin-bottom: 30px; }
.post-content h2 { font-size: 32px; }
@media screen and (max-width: 800px) { .post-content h2 { font-size: 28px; } }
.post-content h3 { font-size: 26px; }
@media screen and (max-width: 800px) { .post-content h3 { font-size: 22px; } }
.post-content h4 { font-size: 20px; }
@media screen and (max-width: 800px) { .post-content h4 { font-size: 18px; } }

/** Syntax highlighting styles */
.highlight { background: #fff; }
.highlighter-rouge .highlight { background: #eef; }
.highlight .c { color: #998; font-style: italic; }
.highlight .err { color: #a61717; background-color: #e3d2d2; }
.highlight .k { font-weight: bold; }
.highlight .o { font-weight: bold; }
.highlight .cm { color: #998; font-style: italic; }
.highlight .cp { color: #999; font-weight: bold; }
.highlight .c1 { color: #998; font-style: italic; }
.highlight .cs { color: #999; font-weight: bold; font-style: italic; }
.highlight .gd { color: #000; background-color: #fdd; }
.highlight .gd .x { color: #000; background-color: #faa; }
.highlight .ge { font-style: italic; }
.highlight .gr { color: #a00; }
.highlight .gh { color: #999; }
.highlight .gi { color: #000; background-color: #dfd; }
.highlight .gi .x { color: #000; background-color: #afa; }
.highlight .go { color: #888; }
.highlight .gp { color: #555; }
.highlight .gs { font-weight: bold; }
.highlight .gu { color: #aaa; }
.highlight .gt { color: #a00; }
.highlight .kc { font-weight: bold; }
.highlight .kd { font-weight: bold; }
.highlight .kp { font-weight: bold; }
.highlight .kr { font-weight: bold; }
.highlight .kt { color: #458; font-weight: bold; }
.highlight .m { color: #099; }
.highlight .s { color: #d14; }
.highlight .na { color: #008080; }
.highlight .nb { color: #0086B3; }
.highlight .nc { color: #458; font-weight: bold; }
.highlight .no { color: #008080; }
.highlight .ni { color: #800080; }
.highlight .ne { color: #900; font-weight: bold; }
.highlight .nf { color: #900; font-weight: bold; }
.highlight .nn { color: #555; }
.highlight .nt { color: #000080; }
.highlight .nv { color: #008080; }
.highlight .ow { font-weight: bold; }
.highlight .w { color: #bbb; }
.highlight .mf { color: #099; }
.highlight .mh { color: #099; }
.highlight .mi { color: #099; }
.highlight .mo { color: #099; }
.highlight .sb { color: #d14; }
.highlight .sc { color: #d14; }
.highlight .sd { color: #d14; }
.highlight .s2 { color: #d14; }
.highlight .se { color: #d14; }
.highlight .sh { color: #d14; }
.highlight .si { color: #d14; }
.highlight .sx { color: #d14; }
.highlight .sr { color: #009926; }
.highlight .s1 { color: #d14; }
.highlight .ss { color: #990073; }
.highlight .bp { color: #999; }
.highlight .vc { color: #008080; }
.highlight .vg { color: #008080; }
.highlight .vi { color: #008080; }
.highlight .il { color: #099; }

@font-face { font-family: 'mononoki'; src: url("fonts/mononoki.woff2") format("woff2"), url("fonts/mononoki.woff") format("woff"); }
@font-face { font-family: 'DejaVu Sans Mono'; src: url("fonts/DejaVuSansMono.woff2") format("woff2"), url("fonts/DejaVuSansMono.woff") format("woff"); font-weight: normal; font-style: normal; }
@font-face { font-family: 'FreeMono'; src: url("fonts/FreeMono.woff") format("woff"); font-stretch: normal; font-style: normal; unicode-range: U+20-7E, U+A0-220, U+224-233, U+237, U+250-36F, U+374-375, U+37A, U+37E, U+384-38A, U+38C, U+38E-3A1, U+3A3-3CE, U+3D0-3D6, U+3DA-3DD, U+3F0-3F1, U+3F4-3F5, U+400-47F, U+483-487, U+48A-4FF, U+510-513, U+51A-51F, U+524-527, U+531-556, U+559-55F, U+561-587, U+589-58A, U+58F, U+5B0-5C7, U+5D0-5EA, U+5F0-5F4, U+606-60F, U+61B, U+61E-657, U+659-6D5, U+6EE-6FF, U+10D0-10F5, U+10F9, U+10FB-10FC, U+13A0-13F4, U+16A0-16F0, U+1E00-1E9B, U+1EA0-1EF9, U+1F00-1F15, U+1F18-1F1D, U+1F20-1F45, U+1F48-1F4D, U+1F50-1F57, U+1F59, U+1F5B, U+1F5D, U+1F5F-1F7D, U+1F80-1FB4, U+1FB6-1FC4, U+1FC6-1FD3, U+1FD6-1FDB, U+1FDD-1FEF, U+1FF2-1FF4, U+1FF6-1FFE, U+2000-2064, U+20A1-20B5, U+20B8-20B9, U+20D0-20D2, U+20D6-20D7, U+20DB-20E3, U+20E5-20E6, U+20E8, U+20EA-20EF, U+2100-2109, U+210D-211A, U+211C-211E, U+2120-2122, U+2124, U+2126-2127, U+2129-212B, U+212E, U+2132, U+2135-213B, U+2141-2144, U+214B, U+214D-214E, U+2153-217F, U+2190-21D5, U+21DC-21DD, U+21E6-21E9, U+21F3, U+2200-22F1, U+2300, U+2302-2306, U+2308-2310, U+2312, U+2314-2315, U+2318-2319, U+231C-2327, U+2329-232C, U+2336-237A, U+237C-23B7, U+23BA-23CF, U+23DA-23DB, U+23DE-23DF, U+23E2-23E6, U+2400-2426, U+2440-244A, U+2460-2469, U+2500-2609, U+2610-2614, U+261A-261F, U+2626-2629, U+262E-2653, U+2660-2667, U+2669-266F, U+2680-2685, U+27C0-27CA, U+27CC, U+27D0-27D7, U+27E4-27EB, U+27F2-27F3, U+27F5-27FC, U+2800-28FF, U+2A00-2A06, U+2A1D, U+2A3F, U+2B00-2B0D, U+2B12-2B19, U+2B1B-2B2B, U+2B53-2B54, U+2E16-2E18, U+2E1A-2E1B, U+2E1E-2E1F, U+2E28-2E2E, U+2E30, U+A788-A78C, U+A900-A92F, U+FB00-FB05, U+FB1D-FB36, U+FB38-FB3C, U+FB3E, U+FB40-FB41, U+FB43-FB44, U+FB46-FBBE, U+FBC0-FBC1, U+FBD3-FBE9, U+FBFC-FBFF, U+FE70-FE74, U+FE76-FEFC, U+FEFF, U+FFF9-FFFD; }
a, a:-webkit-any-link, a:link, a:toc-entry { color: #2a7ae2; text-decoration: none; }

a:visited { color: #1756a9; }

a:hover { color: #111; text-decoration: underline; }

/* Code. */
pre.highlight { padding: .4em .4em !important; background: #e8f2fb !important; border: 1px solid #c9e1f6; border-radius: 3px !important; border-style: dashed !important; }

code { font-family: 'DejaVu Sans Mono', 'Source Code Pro', 'Bitstream Vera Sans Mono', 'FreeMono', 'Courier New', 'Monaco', 'Menlo', monospace, serif !important; font-size: .85em !important; }

/* Agda. */
pre.Agda { font-family: 'DejaVu Sans Mono', 'Source Code Pro', 'Bitstream Vera Sans Mono', 'FreeMono', 'Courier New', 'Monaco', 'Menlo', monospace, serif !important; font-size: .85em !important; padding: .4em .4em !important; background: #e8f2fb !important; border: 1px solid #c9e1f6; border-radius: 3px !important; }

pre.Spec { font-family: 'DejaVu Sans Mono', 'Source Code Pro', 'Bitstream Vera Sans Mono', 'FreeMono', 'Courier New', 'Monaco', 'Menlo', monospace, serif !important; font-size: .85em !important; padding: .4em .4em !important; background: #e8f2fb !important; border: 1px solid #c9e1f6; border-radius: 3px !important; border-style: dashed !important; color: #B22222; }

/* Aspects. */
.Comment { color: #B22222; }

.Keyword { color: #CD6600; }

.String { color: #B22222; }

.Number { color: #A020F0; }

.Symbol { color: #404040; }

.PrimitiveType { color: #0000CD; }

/* NameKinds. */
.Bound { color: black; }

.InductiveConstructor { color: #008B00; }

.CoinductiveConstructor { color: #8B7500; }

.Datatype { color: #0000CD; }

.Field { color: #EE1289; }

.Function { color: #0000CD; }

.Module { color: #A020F0; }

.Postulate { color: #0000CD; }

.Primitive { color: #0000CD; }

.Record { color: #0000CD; }

/* OtherAspects. */
.UnsolvedMeta { color: black; background: yellow; }

.UnsolvedConstraint { color: black; background: yellow; }

.TerminationProblem { color: black; background: #FFA07A; }

.IncompletePattern { color: black; background: #F5DEB3; }

.Error { color: red; text-decoration: underline; }

.TypeChecks { color: black; background: #ADD8E6; }

/* Standard attributes. */
.Agda a { text-decoration: none; }

.Agda a[href]:hover { background-color: #B4EEB4; }

/* BASICS */
.CodeMirror { /* Set height, width, borders, and global font properties here */ font-family: 'DejaVu Sans Mono', 'Source Code Pro', 'Bitstream Vera Sans Mono', 'FreeMono', 'Courier New', 'Monaco', 'Menlo', monospace, serif !important; font-size: .85em !important; height: 300px; direction: ltr; -webkit-tap-highlight-color: black; }

.CodeMirror-foldmarker { visibility: hidden; display: none; }

/* PADDING */
.CodeMirror-lines { padding: 4px 0; /* Vertical padding around content */ }

.CodeMirror pre.CodeMirror-line, .CodeMirror pre.CodeMirror-line-like { padding: 0 4px; /* Horizontal padding of content */ }

.CodeMirror-lines .readOnly { background-color: #cccccc !important; }

.CodeMirror-scrollbar-filler, .CodeMirror-gutter-filler { background-color: white; /* The little square between H and V scrollbars */ }

/* GUTTER */
.CodeMirror-gutters { border-right: 1px solid #ddd; background-color: #dcdcec !important; white-space: nowrap; }

.CodeMirror-linenumber { padding: 0 3px 0 5px; min-width: 20px; text-align: right; color: #424242; white-space: nowrap; }

.CodeMirror-guttermarker { color: black; }

.CodeMirror-guttermarker-subtle { color: #999; }

/* CURSOR */
.CodeMirror-cursor { border-left: 1px solid black; border-right: none; width: 0; }

/* Shown when moving in bi-directional text */
.CodeMirror div.CodeMirror-secondarycursor { border-left: 1px solid silver; }

.cm-fat-cursor .CodeMirror-cursor { width: auto; border: 0 !important; background: #7e7; }

.cm-fat-cursor div.CodeMirror-cursors { z-index: 1; }

.cm-fat-cursor-mark { background-color: rgba(20, 255, 20, 0.5); -webkit-animation: blink 1.06s steps(1) infinite; -moz-animation: blink 1.06s steps(1) infinite; animation: blink 1.06s steps(1) infinite; }

.cm-animate-fat-cursor { width: auto; border: 0; -webkit-animation: blink 1.06s steps(1) infinite; -moz-animation: blink 1.06s steps(1) infinite; animation: blink 1.06s steps(1) infinite; background-color: #7e7; }

@-moz-keyframes blink { 50% { background-color: transparent; } }
@-webkit-keyframes blink { 50% { background-color: transparent; } }
@keyframes blink { 50% { background-color: transparent; } }
/* Can style cursor different in overwrite (non-insert) mode */
.cm-tab { display: inline-block; text-decoration: inherit; }

.CodeMirror-rulers { position: absolute; left: 0; right: 0; top: -50px; bottom: 0; overflow: hidden; }

.CodeMirror-ruler { border-left: 1px solid #ccc; top: 0; bottom: 0; position: absolute; }

/* DEFAULT THEME */
.cm-s-default .cm-header { color: blue; }

.cm-s-default .cm-quote { color: #090; }

.cm-negative { color: #d44; }

.cm-positive { color: #292; }

.cm-header, .cm-strong { font-weight: bold; }

.cm-em { font-style: italic; }

.cm-link { text-decoration: underline; }

.cm-strikethrough { text-decoration: line-through; }

.cm-s-default .cm-keyword { line-height: 1em; color: #CD6600 !important; }

.cm-s-default .cm-atom { color: #219; }

.cm-s-default .cm-number { color: #164; }

.cm-s-default .cm-def { color: #00f; }

/* .cm-s-default .cm-variable {color: #0000CD !important;} */
.cm-s-default .cm-variable-2 { color: #05a; }

.cm-s-default .cm-variable-3, .cm-s-default .cm-type { color: #085; }

.cm-s-default .cm-comment { color: #B22222 !important; }

.cm-s-default .cm-string { color: #a11; }

.cm-s-default .cm-string-2 { color: #f50; }

.cm-s-default .cm-meta { color: #555; }

.cm-s-default .cm-qualifier { color: #555; }

/* .cm-s-default .cm-builtin {color: #30a;} */
.cm-s-default .cm-builtin { color: #0000CD !important; }

.cm-s-default .cm-bracket { color: #997; }

.cm-s-default .cm-tag { color: #170; }

.cm-s-default .cm-attribute { color: #00c; }

.cm-s-default .cm-hr { color: #999; }

.cm-s-default .cm-link { color: #00c; }

.cm-s-default .cm-error { color: #f00; }

.cm-invalidchar { color: #f00; }

.CodeMirror-composing { border-bottom: 2px solid #cecedd; }

/* Default styles for common addons */
div.CodeMirror span.CodeMirror-matchingbracket { color: #0b0; }

div.CodeMirror span.CodeMirror-nonmatchingbracket { color: #a22; }

.CodeMirror-matchingtag { background: rgba(255, 150, 0, 0.3); }

.CodeMirror-activeline-background { background: #e8f2fb !important; }

/* STOP */
/* The rest of this file contains styles related to the mechanics of the editor. You probably shouldn't touch them. */
.CodeMirror { position: relative; overflow: hidden; background: #eeeeff !important; }

.CodeMirror-scroll { overflow: scroll !important; /* Things will break if this is overridden */ /* 50px is the magic margin used to hide the element's real scrollbars */ /* See overflow: hidden in .CodeMirror */ margin-bottom: -50px; margin-right: -50px; padding-bottom: 50px; height: 100%; outline: none; /* Prevent dragging from highlighting the element */ position: relative; }

.CodeMirror-sizer { position: relative; border-right: 50px solid transparent; }

/* The fake, visible scrollbars. Used to force redraw during scrolling before actual scrolling happens, thus preventing shaking and flickering artifacts. */
.CodeMirror-vscrollbar, .CodeMirror-hscrollbar, .CodeMirror-scrollbar-filler, .CodeMirror-gutter-filler { position: absolute; z-index: 6; display: none; }

.CodeMirror-vscrollbar { right: 0; top: 0; overflow-x: hidden; overflow-y: scroll; }

.CodeMirror-hscrollbar { bottom: 0; left: 0; overflow-y: hidden; overflow-x: scroll; }

.CodeMirror-scrollbar-filler { right: 0; bottom: 0; }

.CodeMirror-gutter-filler { left: 0; bottom: 0; }

.CodeMirror-gutters { position: absolute; left: 0; top: 0; min-height: 100%; z-index: 3; }

.CodeMirror-gutter { white-space: normal; height: 100%; display: inline-block; vertical-align: top; margin-bottom: -50px; }

.CodeMirror-gutter-wrapper { position: absolute; z-index: 4; background: none !important; border: none !important; }

.CodeMirror-gutter-background { position: absolute; top: 0; bottom: 0; z-index: 4; }

.CodeMirror-gutter-elt { position: absolute; cursor: default; z-index: 4; }

.CodeMirror-gutter-wrapper ::selection { background-color: #d3e7f8 !important; }

.CodeMirror-gutter-wrapper ::-moz-selection { background-color: #d3e7f8 !important; }

.CodeMirror-lines { cursor: text; min-height: 1px; /* prevents collapsing before first draw */ }

.CodeMirror pre.CodeMirror-line, .CodeMirror pre.CodeMirror-line-like { /* Reset some styles that the rest of the page might have set */ -moz-border-radius: 0; -webkit-border-radius: 0; border-radius: 0; border-width: 0; margin: 0; white-space: pre; word-wrap: normal; line-height: inherit; color: inherit; z-index: 2; position: relative; overflow: visible; -webkit-tap-highlight-color: transparent; -webkit-font-variant-ligatures: contextual; font-variant-ligatures: contextual; }

.CodeMirror-wrap pre.CodeMirror-line, .CodeMirror-wrap pre.CodeMirror-line-like { word-wrap: break-word; white-space: pre-wrap; word-break: normal; }

.CodeMirror-linebackground { position: absolute; left: 0; right: 0; top: 0; bottom: 0; z-index: 0; }

.CodeMirror-linewidget { position: relative; z-index: 2; padding: 0.1px; /* Force widget margins to stay inside of the container */ }

.CodeMirror-rtl pre { direction: rtl; }

.CodeMirror-code { outline: none; }

/* Force content-box sizing for the elements where we expect it */
.CodeMirror-scroll, .CodeMirror-sizer, .CodeMirror-gutter, .CodeMirror-gutters, .CodeMirror-linenumber { -moz-box-sizing: content-box; box-sizing: content-box; }

.CodeMirror-measure { position: absolute; width: 100%; height: 0; overflow: hidden; visibility: hidden; }

.CodeMirror-cursor { position: absolute; pointer-events: none; }

.CodeMirror-measure pre { position: static; }

div.CodeMirror-cursors { visibility: hidden; position: relative; z-index: 3; }

div.CodeMirror-dragcursors { visibility: visible; }

.CodeMirror-focused div.CodeMirror-cursors { visibility: visible; }

.CodeMirror-selected { background: #d3e7f8 !important; }

.CodeMirror-focused .CodeMirror-selected { background: #d3e7f8 !important; border-color: #cce7ff !important; }

.CodeMirror-crosshair { cursor: crosshair; }

.CodeMirror-line::selection, .CodeMirror-line > span::selection, .CodeMirror-line > span > span::selection { background: #d3e7f8; }

.CodeMirror-line::-moz-selection, .CodeMirror-line > span::-moz-selection, .CodeMirror-line > span > span::-moz-selection { background: #d3e7f8; }

span.CodeMirror-selectedtext { background: #d3e7f8 !important; }

.cm-searching { background-color: #ffa; background-color: rgba(255, 255, 0, 0.4); }

/* Used to force a border model for a node */
.cm-force-border { padding-right: .1px; }

@media print { /* Hide the cursor when printing */
  .CodeMirror div.CodeMirror-cursors { visibility: hidden; } }
/* See issue #2901 */
.cm-tab-wrap-hack:after { content: ''; }

.p-Widget, .lm-Widget { box-sizing: border-box; position: relative; overflow: visible !important; cursor: default; }

/* agda-specific extensions */
.compile-error { background: #ff9696 !important; color: black !important; margin-right: -5px; }

.compile-error:link { color: black; }

.compile-ok { background: #e1ffe1 !important; border-radius: 3px; }

.compile-ok-border { border: 1px solid #cde9cc !important; }

.compile-hole { background: #ffffe1; margin-right: -5px; /* !important; */ }

.play-button-class { background-color: transparent; background-repeat: no-repeat; background-size: 10px; background-position: center; border: none; mix-blend-mode: multiply; display: inline-block; vertical-align: middle; line-height: normal; height: 15px; width: 15px; transition: all .3s ease-in-out; filter: blur(0.2px); background-image: url(../assets/images/play.png); padding-left: 5px; padding-right: 12px; border-right: 1px solid #aaaaaa; border-radius: 0px; }

.play-button-class:hover { filter: brightness(130%); cursor: pointer; }

.kernel-status-button { background-color: transparent; background-repeat: no-repeat; background-size: 10px; background-position: center; border: none; mix-blend-mode: multiply; display: inline-block; vertical-align: middle; line-height: normal; height: 15px; width: 15px; transition: all .3s ease-in-out; filter: blur(0.2px); background-image: url(../assets/images/kernel.png); background-size: 25px; height: 25px; width: 25px; transition: none; padding: 5px; border: 0; filter: opacity(25%); -webkit-appearance: button; outline: transparent; }

button.kernel-status-button:hover { cursor: pointer; }

button.kernel-status-button-connected { filter: opacity(100%); }

button.kernel-status-button-disconnected { background-image: url(../assets/images/kernel-broken.png); filter: opacity(100%); }

.status-badge-error { width: 15px; height: 15px; border-radius: 50%; margin-top: 5px; float: right; stroke-width: 4; stroke: #fff; stroke-miterlimit: 10; stroke-width: 1; }

.status-badge-warning { width: 15px; height: 15px; border-radius: 50%; margin-top: 5px; float: right; stroke-width: 4; stroke: #fff; stroke-miterlimit: 10; stroke-width: 1; }

.status-badge-ok { width: 15px; height: 15px; border-radius: 50%; margin-top: 5px; float: right; stroke-width: 4; stroke: #fff; stroke-miterlimit: 10; box-shadow: inset 0px 0px 0px #7ac142; animation: fill .4s ease-in-out .4s forwards, scale .3s ease-in-out .9s both; }

.info-area { display: none; }

svg.status-badge-warning:hover { cursor: pointer; display: block; visibility: visible; }

.checkmark__circle { stroke-dasharray: 166; stroke-dashoffset: 166; stroke-width: 2; stroke-miterlimit: 10; stroke: #7ac142; fill: none; animation: stroke 0.6s cubic-bezier(0.65, 0, 0.45, 1) forwards; }

.checkmark__check { transform-origin: 50% 50%; stroke-dasharray: 48; stroke-dashoffset: 48; animation: stroke 0.3s cubic-bezier(0.65, 0, 0.45, 1) 0.8s forwards; }

@keyframes stroke { 100% { stroke-dashoffset: 0; } }
@keyframes scale { 0%, 100% { transform: none; }
  50% { transform: scale3d(1.1, 1.1, 1); } }
@keyframes fill { 100% { box-shadow: inset 0px 0px 0px 30px #7ac142; } }
.status-badge-running { width: 15px; height: 15px; border-radius: 50%; margin-top: 5px; float: right; stroke-width: 4; stroke: #fff; stroke-miterlimit: 10; box-shadow: inset 0px 0px 0px 30px #ec9f6e; animation: lds-heart 1.5s infinite cubic-bezier(0.215, 0.61, 0.355, 1); }

.running__circle { stroke-dasharray: 166; stroke-dashoffset: 166; stroke-width: 2; stroke-miterlimit: 10; stroke: #ec9f6e; fill: #ec9f6e; animation: fill-running 0.6s cubic-bezier(0.65, 0, 0.45, 1) forwards; }

@keyframes fill-running { 100% { box-shadow: inset 0px 0px 0px 30px #ec9f6e; } }
.status-badge-unknown { width: 15px; height: 15px; border-radius: 50%; margin-top: 5px; float: right; stroke-width: 4; stroke: #fff; stroke-miterlimit: 10; box-shadow: inset 0px 0px 0px 30px #94959f; fill: #94959f; }

@keyframes fill-unknown { 100% { box-shadow: inset 0px 0px 0px 30px #94959f; } }
.unknown__circle { stroke-dasharray: 166; stroke-dashoffset: 166; stroke-width: 2; stroke-miterlimit: 10; stroke: #94959f; fill: #94959f; }

@keyframes lds-dual-ring { 0% { transform: rotate(0deg); }
  100% { transform: rotate(360deg); } }
@keyframes lds-heart { 0% { transform: scale(0.95); }
  5% { transform: scale(1.1); }
  39% { transform: scale(0.85); }
  45% { transform: scale(1); }
  60% { transform: scale(0.95); }
  100% { transform: scale(0.9); } }
@keyframes pulse { 0% { transform: scale(0.95); box-shadow: 0 0 0 0 rgba(0, 0, 0, 0.7); }
  70% { transform: scale(1); box-shadow: 0 0 0 10px rgba(0, 0, 0, 0); }
  100% { transform: scale(0.95); box-shadow: 0 0 0 0 rgba(0, 0, 0, 0); } }
.thebelab-cell { padding: 0px; background: #eeeeff; border: 2px solid #e0dede; border-radius: 3px; }

.thebelab-cell { /* border: 2px solid #aaa;
border-radius: 4px;
margin-top: 8px;
margin-bottom: 8px; */ transition: all .1s ease-in-out; }

.thebelab-cell:hover { padding: 0px; border: 2px solid #cccbcb; }

.thebelab-cell:focus-within { padding: 0px; border: 2px solid #888787; }

.jp-OutputArea { padding: 0px; }

.jp-OutputArea > :first-child { padding-top: 0em; border-top: 1px solid #cecfdd; }

.jp-OutputArea-output { padding: 8px; }

.jp-RenderedText pre, .jp-RenderedJavaScript pre, .jp-RenderedHTMLCommon pre { margin-bottom: 0px; }

.thebelab-input { border-bottom: 1px solid #cecedd; }

main { padding: 0; }

header.site-header { position: sticky; top: 0; width: 100%; height: 50px; z-index: 10; padding-bottom: 5px; background: white; -webkit-box-shadow: 0 7px 8px rgba(0, 0, 0, 0.12); -moz-box-shadow: 0 7px 8px rgba(0, 0, 0, 0.12); box-shadow: 0 7px 8px rgba(0, 0, 0, 0.12); text-align: center; border-top: none; min-height: 0; transition: top 0.3s; /* Transition effect when sliding down (and up) */ }

content > div { height: 50px; }

.tooltip { position: relative; display: inline-block; z-index: 100; }

.tooltip .tooltiptext { opacity: 0; visibility: hidden; background-color: #494949; color: #e2e2e2; border-radius: 6px; z-index: 1000; position: fixed; padding: 10px; top: 150%; width: 120px; text-align: center; /* Position the tooltip */ top: -6px; margin-left: 15px; padding: 5px; }

.tooltip:hover .tooltiptext { opacity: 1; }

span.cell-count { text-align: center; height: 10px; position: absolute; top: 125%; line-height: normal; background: transparent; }

span.kernel-messages { opacity: 0; visibility: hidden; background-color: #494949; color: #e2e2e2; border-radius: 6px; z-index: 1000; position: fixed; padding: 10px; top: 150%; width: 600px; text-align: left; z-index: 100; margin-left: -600px; height: 250px; overflow: auto; top: 125%; position: absolute; line-height: normal; opacity: 50%; }

span.kernel-status:hover span.kernel-messages { visibility: visible; opacity: 1; filter: opacity(100%) !important; }

.cell-info { color: #808080; display: inline-block; vertical-align: middle; line-height: normal; padding-left: 10px; display: inline-block; font-size: 10pt; }

div.cell-toolbar { padding: 5px; }

pre { background-color: transparent; border: none; }

.info-area-button { cursor: pointer; position: absolute; bottom: 0px; right: 5px; visibility: hidden; }

.show-info-area { content: url("../assets/images/show.svg"); }

.hide-info-area { content: url("../assets/images/hide.svg"); }

.trigger { display: none; }

@media screen and (min-width: 600px) { .trigger { display: block; } }
ul.list-of-contributors { display: grid; grid-template-columns: repeat(3, 1fr); width: calc(100% - 2rem); }

ul.list-of-contributors li { margin-right: 2rem; }

pre { break-inside: avoid; }

.post-title { font-size: 3em; margin-top: 0em; }

h1, h2, h3, h4, h5, h6 { color: #111; line-height: 125%; margin-top: 0em; font-weight: normal; }

.post-content h1 { font-size: 2.5em; margin-top: 0em; }

dt { display: inline; }

dd { display: inline; }

.exercise:after { display: inline-block; content: "."; }

.example:after { display: inline-block; content: "."; }

.theorem:after { display: inline-block; content: "."; }

.lemma:after { display: inline-block; content: "."; }

body { overflow-wrap: break-word; text-align: justify; }

.post-content h1:before { content: ""; border-top: 1px dashed rgba(0, 0, 0, 0); display: block; position: relative; justify-content: center; text-align: center; font-size: 1em; margin-top: 1em; margin-right: 2em; margin-bottom: 0.5em; margin-left: 2em; }

h4, h5, h6 { font-weight: bold; }

h2 { font-size: 2em; margin-top: 1.1em; }

h3 { font-size: 1.5em; margin-top: 1em; }

h4 { font-size: 1.2em; }

h5 { font-size: 1em; }

h6 { font-size: 0.9em; }

.reversefootnote { visibility: hidden; position: relative; }

.reversefootnote:after { visibility: visible; position: absolute; top: 0; left: 0; content: "\21B5"; }

.theorembox { position: relative; }

.lemmabox { position: relative; }

.remarkbox { position: relative; }

.examplebox { position: relative; }

.inlinecode { display: block; }

.inlinecode p { display: inline !important; }

.inlinecode pre { display: inline !important; background: transparent; border: none; white-space: nowrap; padding: 2px 3px; word-spacing: -3px; }

.solutionbox { position: relative; }

.exercisebox { position: relative; }

.center { text-align: center; }

pre.highlight { padding: .4em .4em; background: #e8f2fb; border: 1px solid #e0dede; border-radius: 3px; border-style: solid !important; }

.collapsible { background-color: #ffffff; cursor: pointer; margin: 0px; padding: 0px; border: none; text-align: right; outline: none; display: inline; position: absolute; right: 0em; font: inherit; }

.right-aligned { display: inline; position: absolute; right: 0em; }

/* Add a background color to the button if it is clicked on (add the .active class with JS), and when you move the mouse over it (hover) */
.active, .collapsible:hover { font: normal; }

/* Style the collapsible content. Note: hidden by default */
.hidebox { padding: 0 0px; display: none; overflow: hidden; }

.flex-box { display: flex; justify-content: space-between; align-items: flex-end; }

.introbox { position: relative; }

div .solutionlink { text-align: end; }

.hidden { visibility: hidden; }

.highlighter-rouge .highlight { background: #eef !important; }