💾 Archived View for gemlog.blue › users › jiaming › 1606832180.gmi captured on 2024-07-09 at 04:34:00. Gemini links have been rewritten to link to archived content
⬅️ Previous capture (2021-12-04)
-=-=-=-=-=-=-
01/12/2020 (things i learned)
- Proved `nat.fact` is primitive recursive in Lean!
- Know what CIC (calculus of inductive constructions) and
Strong Normalization Property means
- revise mathlib's implementation of primrec
- Grokxzlkjzy's (not actual name so not counted) heirarchy
basically just +, x, ^, tetration, .... (super cool)
- .elan runs away from my $PATH every time i log in hmmm