| Pronouns | he/him |
| Pronunciation | Sung (sing/sang/*sung) Hun (*hon*ey) |
The shrubbery grouping rules are very subtle. Namely, the relationship between newlines, indentation, separators, and opener-closer pairs get really crazy. (1,\n 2, 3), (\n1, 2, 3) (1:\n 2,\n 3) work, but (1,\n2,3) does not.
The documentation does not help too much either here because unlike the tokenization guide, the guide about grouping is mostly informal prose.
Pleased to live in a place where this is true (enough):
Eight states received “A” grades for LGBTQ+ safety based on their comprehensive pro-equality laws and low rates of hate crimes against LGBTQ+ people. **Only Rhode Island nabbed an A+ mark.**
https://www.safehome.org/data-lgbtq-state-safety-rankings/
Another cool Lean exercise: a verified implementation of the Boyer-Moore majority voting algorithm.
It's an O(n) time O(1) space majority element detection algorithm.
The 1981 verification of took the authors 20 hours. In contrast, I spent no more than 4 hours (including building the CLI tool) thanks to proof automation techniques like grind and omega.
I wrote my first non-trivial Lean program with proof of correctness: the Karatsuba algorithm for "fast" arbitrary precision multiplication.
I implemented the algorithm in Lean and proved it was equivalent to vanilla multiplication.
I'm wondering how difficult it would be to also reason about the algorithm's asymptotic runtime. I already wrote a reasonably involved termination proof, so maybe I can reuse some of that machinery
Shriram Krishnamurthi
