lean4-htt/doc/pygments.css
Chris Lovett cc95456639
doc: add documentation on monads (#1505)
* doc: add documentation on functors.

* fix: make comments green

* minor tweaks

* doc: add section on Applicatives.

* doc: add some more info on the laws from Mario.

* doc: add law list and move lazy evaluation up so the chapter ends properly.

* doc: Add something on seqLeft and seqRight.

* doc: add section on monads.

* doc: fix some typos.

* doc: switch to LeanInk for chaper on Monads.

* doc: remove old files.

* doc: fix mdbook test errors.

* doc: add part 4: readers

* doc: add section on State monads

* doc: fix some typos and add some more details.

* doc: fix typos and add some CR feedback.

* doc: add Except monad section.

* doc: add info on monad transformers.

* Delete transformers.lean.md

* doc: fix some typos.

* doc: fix typos and move forward reference to monad lifting.

* doc: Update `State` to `StateM`

* doc: fix references to State to become StateM.

* doc: generalize indexOf implementation.

* doc: add chapter on monad laws and move "law" sections to this chapter to avoid redundancy.

* doc: add theorem

* Delete laws.lean.md

* doc: fix some typos.

* doc: fix broken link.

* doc: fox typos.

* fix: language changed from "us" to "you".

* doc: fix code review comments.

* doc: some word smithing

* doc: some word smithing and sample simplification.

* doc: add bad_option_map example.

* doc: add side note on `return` statement and fix heading level consistency.

* Add `withReader` info

* doc: change language from us, our, your, we, we'll, we've to "you"

* doc: add some forward links.

* doc: put spaces around colon in function  arguments like "(x : List Nat)"

* doc:
Add backticks on map
Remove commands on multiline structure instance
Fix centerdot
Add "one of"

* doc: Remove info about Functor in other languages.

* doc:
add info on <$> being left associative
remove another forward reference to monad
fix typo `operatoions`
remove unneccesary parens after <$>

* doc:
fix Type u -> Type v
fix you -> your
use `let val? ← IO.getEnv name`
in Readers call it "context" rather than "state".

* doc: fix withReader docs
use 'context' to describe the ReaderM state.
remove "trivial"
type inference => Lean
"abstract classes" => "abstract structures"
remove unnecessary parens

* doc: fix bug in explanation of `let x ← readerFunc2`
Fix explanation of equivalence between `def f (a : Nat) : String` and `def f : Nat → String`

* doc: move hasSomeItemGreaterThan to Except.lean
Add validateList List.anyM example.
fix `def f (a : Nat) : String` language.

* doc: fix "What transformation are you referring to"

* doc: fix typo.

* doc: add missing period.

* doc: fix validateList

* doc: explain `λ` notation.

* doc: reword the map, seq, bind comparison.

* doc: fix some more 'reader state' to 'reader context' language

* doc: fix wrote statement about return only works in do blocks.

* doc: fix typo

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

* doc: improve language

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

* doc: fix typo

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

* Add info on what a do block is doing for you.

* doc: define definitionally equal

* doc: make `readerFunc3.run env` canonical.

* doc: remove unnecessary parens.

* doc: fix typos

* doc: make List.map a bit more clear in the intro to Functors.

* doc: simplify readerFunc3WithReader

* doc: switch to svg for diagram so it works better on dark themes.

* doc: align nodes in diagram and convert to svg.

* doc: simplify playGame using while true.

* doc: drop confusing statement about "definitionally equal"

* doc: switch to `import Lean.Data.HashMap`

* doc: fix typo "operatoins"

* doc: update diagram to add more info and polish the intro paragraphs so they better match the actual contents of each chapter.

* doc: fix typo

* doc: fix typo.

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
2022-09-05 13:33:15 -07:00

83 lines
No EOL
6.1 KiB
CSS

/* Pygments stylesheet generated by Alectryon (style=None) */
td.linenos .normal { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }
span.linenos { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }
td.linenos .special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }
span.linenos.special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }
.highlight .hll, .code .hll { background-color: #ffffcc }
.highlight .c, .code .c { color: #555753; font-style: italic } /* Comment */
.highlight .err, .code .err { color: #a40000; border: 1px solid #cc0000 } /* Error */
.highlight .g, .code .g { color: #000000 } /* Generic */
.highlight .k, .code .k { color: #8f5902 } /* Keyword */
.highlight .l, .code .l { color: #2e3436 } /* Literal */
.highlight .n, .code .n { color: #000000 } /* Name */
.highlight .o, .code .o { color: #000000 } /* Operator */
.highlight .x, .code .x { color: #2e3436 } /* Other */
.highlight .p, .code .p { color: #000000 } /* Punctuation */
.highlight .ch, .code .ch { color: #555753; font-weight: bold; font-style: italic } /* Comment.Hashbang */
.highlight .cm, .code .cm { color: #555753; font-style: italic } /* Comment.Multiline */
.highlight .cp, .code .cp { color: #3465a4; font-style: italic } /* Comment.Preproc */
.highlight .cpf, .code .cpf { color: #555753; font-style: italic } /* Comment.PreprocFile */
.highlight .c1, .code .c1 { color: #555753; font-style: italic } /* Comment.Single */
.highlight .cs, .code .cs { color: #3465a4; font-weight: bold; font-style: italic } /* Comment.Special */
.highlight .gd, .code .gd { color: #a40000 } /* Generic.Deleted */
.highlight .ge, .code .ge { color: #000000; font-style: italic } /* Generic.Emph */
.highlight .gr, .code .gr { color: #a40000 } /* Generic.Error */
.highlight .gh, .code .gh { color: #a40000; font-weight: bold } /* Generic.Heading */
.highlight .gi, .code .gi { color: #4e9a06 } /* Generic.Inserted */
.highlight .go, .code .go { color: #000000; font-style: italic } /* Generic.Output */
.highlight .gp, .code .gp { color: #8f5902 } /* Generic.Prompt */
.highlight .gs, .code .gs { color: #000000; font-weight: bold } /* Generic.Strong */
.highlight .gu, .code .gu { color: #000000; font-weight: bold } /* Generic.Subheading */
.highlight .gt, .code .gt { color: #000000; font-style: italic } /* Generic.Traceback */
.highlight .kc, .code .kc { color: #204a87; font-weight: bold } /* Keyword.Constant */
.highlight .kd, .code .kd { color: #4e9a06; font-weight: bold } /* Keyword.Declaration */
.highlight .kn, .code .kn { color: #4e9a06; font-weight: bold } /* Keyword.Namespace */
.highlight .kp, .code .kp { color: #204a87 } /* Keyword.Pseudo */
.highlight .kr, .code .kr { color: #8f5902 } /* Keyword.Reserved */
.highlight .kt, .code .kt { color: #204a87 } /* Keyword.Type */
.highlight .ld, .code .ld { color: #2e3436 } /* Literal.Date */
.highlight .m, .code .m { color: #2e3436 } /* Literal.Number */
.highlight .s, .code .s { color: #ad7fa8 } /* Literal.String */
.highlight .na, .code .na { color: #c4a000 } /* Name.Attribute */
.highlight .nb, .code .nb { color: #75507b } /* Name.Builtin */
.highlight .nc, .code .nc { color: #204a87 } /* Name.Class */
.highlight .no, .code .no { color: #ce5c00 } /* Name.Constant */
.highlight .nd, .code .nd { color: #3465a4; font-weight: bold } /* Name.Decorator */
.highlight .ni, .code .ni { color: #c4a000; text-decoration: underline } /* Name.Entity */
.highlight .ne, .code .ne { color: #cc0000 } /* Name.Exception */
.highlight .nf, .code .nf { color: #a40000 } /* Name.Function */
.highlight .nl, .code .nl { color: #3465a4; font-weight: bold } /* Name.Label */
.highlight .nn, .code .nn { color: #000000 } /* Name.Namespace */
.highlight .nx, .code .nx { color: #000000 } /* Name.Other */
.highlight .py, .code .py { color: #000000 } /* Name.Property */
.highlight .nt, .code .nt { color: #a40000 } /* Name.Tag */
.highlight .nv, .code .nv { color: #ce5c00 } /* Name.Variable */
.highlight .ow, .code .ow { color: #8f5902 } /* Operator.Word */
.highlight .w, .code .w { color: #d3d7cf; text-decoration: underline } /* Text.Whitespace */
.highlight .mb, .code .mb { color: #2e3436 } /* Literal.Number.Bin */
.highlight .mf, .code .mf { color: #2e3436 } /* Literal.Number.Float */
.highlight .mh, .code .mh { color: #2e3436 } /* Literal.Number.Hex */
.highlight .mi, .code .mi { color: #2e3436 } /* Literal.Number.Integer */
.highlight .mo, .code .mo { color: #2e3436 } /* Literal.Number.Oct */
.highlight .sa, .code .sa { color: #ad7fa8 } /* Literal.String.Affix */
.highlight .sb, .code .sb { color: #ad7fa8 } /* Literal.String.Backtick */
.highlight .sc, .code .sc { color: #ad7fa8; font-weight: bold } /* Literal.String.Char */
.highlight .dl, .code .dl { color: #ad7fa8 } /* Literal.String.Delimiter */
.highlight .sd, .code .sd { color: #ad7fa8 } /* Literal.String.Doc */
.highlight .s2, .code .s2 { color: #ad7fa8 } /* Literal.String.Double */
.highlight .se, .code .se { color: #ad7fa8; font-weight: bold } /* Literal.String.Escape */
.highlight .sh, .code .sh { color: #ad7fa8; text-decoration: underline } /* Literal.String.Heredoc */
.highlight .si, .code .si { color: #ce5c00 } /* Literal.String.Interpol */
.highlight .sx, .code .sx { color: #ad7fa8 } /* Literal.String.Other */
.highlight .sr, .code .sr { color: #ad7fa8 } /* Literal.String.Regex */
.highlight .s1, .code .s1 { color: #ad7fa8 } /* Literal.String.Single */
.highlight .ss, .code .ss { color: #8f5902 } /* Literal.String.Symbol */
.highlight .bp, .code .bp { color: #5c35cc } /* Name.Builtin.Pseudo */
.highlight .fm, .code .fm { color: #a40000 } /* Name.Function.Magic */
.highlight .vc, .code .vc { color: #ce5c00 } /* Name.Variable.Class */
.highlight .vg, .code .vg { color: #ce5c00; text-decoration: underline } /* Name.Variable.Global */
.highlight .vi, .code .vi { color: #ce5c00 } /* Name.Variable.Instance */
.highlight .vm, .code .vm { color: #ce5c00 } /* Name.Variable.Magic */
.highlight .il, .code .il { color: #2e3436 } /* Literal.Number.Integer.Long */
.hljs-doctag { color: green }
.hljs-comment { color: green }