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