From 5c7072887f01ae5a1795942f5ab8ecab6d47d9ac Mon Sep 17 00:00:00 2001
From: GitHub Actions Bot <>
Date: Sat, 28 Jan 2023 23:21:46 +0000
Subject: [PATCH] New/Modified Toots

---
 109764840432564992.md | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 109764840432564992.md

diff --git a/109764840432564992.md b/109764840432564992.md
new file mode 100644
index 0000000..4f4ac8e
--- /dev/null
+++ b/109764840432564992.md
@@ -0,0 +1,6 @@
+---
+{"id": "109764840432564992", "in_reply_to_id": null, "in_reply_to_account_id": null, "sensitive": false, "spoiler_text": "", "visibility": "public", "language": "en", "replies_count": 0, "reblogs_count": 0, "favourites_count": 0, "edited_at": null, "reblog": null, "application": null, "account": {"id": "108219415927856966", "username": "brozek", "acct": "brozek", "display_name": "Brandon Rozek", "url": "https://fosstodon.org/@brozek", "avatar": "https://cdn.fosstodon.org/accounts/avatars/108/219/415/927/856/966/original/bae9f46f23936e79.jpg", "avatar_static": "https://cdn.fosstodon.org/accounts/avatars/108/219/415/927/856/966/original/bae9f46f23936e79.jpg", "header": "https://fosstodon.org/headers/original/missing.png", "header_static": "https://fosstodon.org/headers/original/missing.png", "noindex": true}, "media_attachments": [], "mentions": [], "tags": [{"name": "leanprover", "url": "https://fosstodon.org/tags/leanprover"}, {"name": "itp", "url": "https://fosstodon.org/tags/itp"}, {"name": "formalmethods", "url": "https://fosstodon.org/tags/formalmethods"}], "emojis": [], "card": {"url": "https://brandonrozek.com/blog/readable-lean3-proofs/", "title": "Readable Lean 3 Proofs", "description": "Important Note: This blog post uses the Lean 3 syntax\nInteractive theorem provers are notorious for showcasing unreadable proofs. Let\u2019s illustrate our point with a couple examples and discuss various ways we can make it more readable.\nDisjunction Elimination Disjunction Elimination or proof by cases is a rule of inference that states the following. Consider you have the following three proofs:\n$p \\vee q$ $p \\rightarrow r$ $q \\rightarrow r$ Then it doesn\u2019t matter if it is $p$ rather than $q$ that holds, in the end $r$ holds.", "type": "link", "author_name": "Brandon Rozek", "author_url": "https://brandonrozek.com/", "provider_name": "", "provider_url": "", "html": "", "width": 0, "height": 0, "image": null, "embed_url": "", "blurhash": null}, "poll": null, "syndication": "https://fosstodon.org/@brozek/109764840432564992", "date": "2023-01-28T04:02:26.641Z"}
+---
+{{< unsafe >}}
+<p>How do you organize your Lean proofs? I wrote a blog post discussing some strategies I employ to make Lean 3 proofs more readable.</p><p><a href="https://brandonrozek.com/blog/readable-lean3-proofs/" target="_blank" rel="nofollow noopener noreferrer"><span class="invisible">https://</span><span class="ellipsis">brandonrozek.com/blog/readable</span><span class="invisible">-lean3-proofs/</span></a></p><p><a href="https://fosstodon.org/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a> <a href="https://fosstodon.org/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://fosstodon.org/tags/FormalMethods" class="mention hashtag" rel="tag">#<span>FormalMethods</span></a></p>
+{{< /unsafe >}}