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