brozek/website
1
0
Fork 0
mirror of https://github.com/Brandon-Rozek/website.git synced 2025-10-10 06:51:13 +00:00
Code Issues Projects Releases Packages Activity

Fixed links

Browse source
This commit is contained in:
Brandon Rozek 2023-09-26 17:43:41 -04:00
parent 18ca6cae06
commit 1bb95f36d7
No known key found for this signature in database
GPG key ID: 26E457DA82C9F480
27 changed files with 100 additions and 100 deletions
Download patch file Download diff file Expand all files Collapse all files

2
content/blog/lean3-tutorial.md
View file

@ -552,4 +552,4 @@ Notice that a couple times in the proof, make use of a tactic called `linarith`.
That concludes the examples I gave for my talk. For each proof, you can see that I included at least two different ways of going about proving it. I generally prefer the inference style method where we explicitely call on `Or.elim` and the like. Though when it comes to double induction, I have not figured out how to apply `rec_on` multiple times in a clean way.
In the process of making this tutorial, I released other lean posts. One that I recommend checking out is ["Readable Lean 3 Proofs"](/blog/readable-lean3-proofs). In it, I give my opinions on how to make the written out proofs more human friendly.
In the process of making this tutorial, I released other lean posts. One that I recommend checking out is ["Readable Lean 3 Proofs"](/blog/readable-lean3-proofs/). In it, I give my opinions on how to make the written out proofs more human friendly.