Commits at 8c3316db1677d40d8f0ef577a32714db345f12e1
-
8c3316db
Random broken binomial stuff
Anthony Wang
authored at
Anthony Wang
comitted at
-
339ffe6f
More cleanup for Sum.lean
Anthony Wang
authored at
Anthony Wang
comitted at
-
9b2a566c
Simplify and clean up Sum.lean
Anthony Wang
authored at
Anthony Wang
comitted at
-
5e38f898
The native_decide proof of false is broken ðŸ˜ðŸ˜ðŸ˜
Anthony Wang
authored at
Anthony Wang
comitted at
-
40c261b9
Don't need to rw definition before use
Anthony Wang
authored at
Anthony Wang
comitted at
-
7e1f8af4
Update Lean and mathlib
Anthony Wang
authored at
Anthony Wang
comitted at
-
4bbd02ce
Simplify proof slightly
Anthony Wang
authored at
Anthony Wang
comitted at
-
3fdf4e82
Finish all the BinOp warmup proofs
Anthony Wang
authored at
Anthony Wang
comitted at
-
9b316070
Remove commented out bad code
Anthony Wang
authored at
Anthony Wang
comitted at
-
41ebc9e4
Random binop math olympiad stuff
Anthony Wang
authored at
Anthony Wang
comitted at
-
e8d49e8d
Add random daofp stuff
Anthony Wang
authored at
Anthony Wang
comitted at
-
4b2644a6
Add multicore gcd thing
Anthony Wang
authored at
Anthony Wang
comitted at
-
e6d348de
Oh huh turns out Nat and â„• are the same thing??
Anthony Wang
authored at
Anthony Wang
comitted at
-
d193e909
Nuke mostly blank README
Anthony Wang
authored at
Anthony Wang
comitted at
-
ebb5f7a5
Use consistent naming scheme, update deps
Anthony Wang
authored at
Anthony Wang
comitted at
-
a550939c
Slight cleanup
Anthony Wang
authored at
Anthony Wang
comitted at
-
32382807
YAYAYAYAYAYYAYYY
Anthony Wang
authored at
Anthony Wang
comitted at
-
279a0619
Only 1 sorry remains!!
Anthony Wang
authored at
Anthony Wang
comitted at
-
b520d528
Use ceil instead of floor
Anthony Wang
authored at
Anthony Wang
comitted at
-
43bda800
Only 3 sorry's remaining
Anthony Wang
authored at
Anthony Wang
comitted at
-
63cce64c
Nearly nearly done
Anthony Wang
authored at
Anthony Wang
comitted at
-
2253e7ca
Nearly done with proof
Anthony Wang
authored at
Anthony Wang
comitted at
-
d4095839
Almost done with double sum proof
Anthony Wang
authored at
Anthony Wang
comitted at
-
9993f661
Random doc examples
Anthony Wang
authored at
Anthony Wang
comitted at
-
b40848ee
Format it nicer
Anthony Wang
authored at
Anthony Wang
comitted at
-
5f8ddee5
Oh oops it's = not ==
Anthony Wang
authored at
Anthony Wang
comitted at
-
d5462456
It's untyped
Anthony Wang
authored at
Anthony Wang
comitted at
-
1e07b2fb
Don't need type signature for sub
Anthony Wang
authored at
Anthony Wang
comitted at
-
882b2859
Make it pretty
Anthony Wang
authored at
Anthony Wang
comitted at
-
84e1082d
Simple lambda calculus interpreter
Anthony Wang
authored at
Anthony Wang
comitted at