Dialog List Item

Dan's Little Books style dialog

To use Dialog List Item extensions, name a item by dialog, like the following:
    What is number?
    0

    Number is about counting.
    1, 2, 3, ...
    We should starting from 0.
    1

    Ok,
    0, 1, 2, 3, ...
    That's much better!
    2

    What's next?
- [dialog]

  - What is number?

  - Number is about counting.

    1, 2, 3, ...

  - We should starting from 0.

  - Ok,

    0, 1, 2, 3, ...

  - That's much better!

  - What's next?

Multiple dialogs in the same document will share the same indexing.
    What's after 3?
    3

    4, 5, 6, ...
    How many numbers are there?
    4

    Infinitely many!
    What is the point of a judgment?
    5

    A judgment is an attitude that a person takes towards expressions. When we come to know something, we are making a judgment.

    1. Thanks, Per Martin-Löf (1942-).
- [dialog]

  - What is the point of a judgment?

  - A judgment is an attitude that a person takes towards expressions.
    When we come to know something, we are making a judgment.

    - Thanks, Per Martin-L6f (1942-).
We can also use Reminder List Item extensions, to render reminder cards of Rules and Laws in the little books:
    Natural Number
    We can construct natural number, by zero and add1.
- [reminder] Natural Number

  - We can construct natural number, by `zero` and `add1`.
Another one, from "The Little Typer":
    Everything Is an Expression
    In some languages (such as Pie), values are also expressions. Evaluation such languages finds an expression, not some other kind of thing.
    Before type theory
    In programming, we do not write types, we only write terms.
    In logic, we do not write terms, we only write types -- propositions and their inference rules.