removed forced sans on quotes
This commit is contained in:
parent
97032c1593
commit
6e88c1a696
2 changed files with 1 additions and 2 deletions
|
@ -30,7 +30,7 @@ theorem fuse {α β γ} : ∀ (xs : List α) (f : α → β) (g :β → γ),
|
|||
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)`.
|
||||
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.
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue