56 lines
No EOL
3.7 KiB
Text
56 lines
No EOL
3.7 KiB
Text
# Evaluate This Style.
|
||
|
||
Abraham Lincoln delivered the Gettysburg Address in 1863 at the dedication of Soldiers' National Cemetery.
|
||
|
||
> Four score and seven years ago our fathers brought forth on this continent, a new nation, conceived in Liberty, and dedicated to the proposition that all men are created equal.
|
||
>
|
||
> Now we are engaged in a great civil war, testing whether that nation, or any nation so conceived and so dedicated, can long endure. We are met on a great battle-field of that war. We have come to dedicate a portion of that field, as a final resting place for those who here gave their lives that that nation might live. It is altogether fitting and proper that we should do this.
|
||
>
|
||
> But, in a larger sense, we can not dedicate --- we can not consecrate --- we can not hallow --- this ground. The brave men, living and dead, who struggled here, have consecrated it, far above our poor power to add or detract. The world will little note, nor long remember what we say here, but it can never forget what they did here. It is for us the living, rather, to be dedicated here to the unfinished work which they who fought here have thus far so nobly advanced. It is rather for us to be here dedicated to the great task remaining before us --- that from these honored dead we take increased devotion to that cause for which they gave the last full measure of devotion --- that we here highly resolve that these dead shall not have died in vain --- that this nation, under God, shall have a new birth of freedom --- and that government of the people, by the people, for the people, shall not perish from the earth.
|
||
|
||
## Djot Syntax
|
||
|
||
We can set block quotes like the above by prefixing each line (including blank ones) with `> `. This is _essentially_ a port from [commonmark](https://commonmark.org/), though as usual, [djot](https://djot.net/) makes minor changes for simplicity and consistency.
|
||
|
||
> .o'i mu xagji sofybakni cu zvati le purdi
|
||
|
||
*Caution.* Five hungry Soviet cows are in the garden.
|
||
|
||
```lean4
|
||
def map' {α β : Type} (f : α → β) : List α → List β
|
||
| [] => []
|
||
| x :: xs => f x :: map' f xs
|
||
|
||
theorem fuse {α β γ} : ∀ (xs : List α) (f : α → β) (g : β → γ),
|
||
(map' g ∘ map' f) xs = map' (g ∘ f) xs := by
|
||
intro xs f g
|
||
induction xs
|
||
. simp [map']
|
||
. rename_i _ _ IH
|
||
simp [map', ←IH, Function.comp]
|
||
```
|
||
|
||
A simple proof of fusion for `List.map` in Lean 4. This and similar theorems are why pure languages like Lean and Haskell can transform e.g. `map f xs |> map g xs` into `map (fun x -> g (f x)) xs`, i.e. `map g . map f` into `map (g . f)`, reducing the number of times a structure must be iterated and thus improving spatial locality.
|
||
|
||
The above block is set with ```` ``` ```` above and below the code. Interestingly, trying to type that little backtick sequence there is a little unintuitive in markdown/djot. If the code you're trying to set has $`n` consecutive backticks in it, you have to surround it with $`n+1` backticks and pad those delimiters inside with a space. 1234567890 is a pretty small number, really.
|
||
|
||
{.thematic}
|
||
***
|
||
|
||
There are ten books in Iain M. Banks' _Culture_ series, possibly the greatest cohesive science-fiction series of all time. Banks' prose and poetry leaves little to be desired.
|
||
|
||
1. Consider Phlebas
|
||
2. The Player of Games
|
||
3. The State of the Art
|
||
4. Use of Weapons
|
||
5. Excession
|
||
6. Inversions
|
||
7. Look to Windward
|
||
8. Matter
|
||
9. Surface Detail
|
||
10. The Hydrogen Sonata
|
||
|
||
Math is something I'm still working on; in more ways than one. Something like $$`\forall x \in \mathbb{N}, x \in \mathbb{N}` is easy enough, but other things are harder.
|
||
Not everyone knows what distfix grammars[^mixfix] are, but they're quite useful when it comes to implementing user-defined syntax.
|
||
|
||
[^mixfix]: Also, perhaps more commonly, called "mixfix" grammars. |