Commit 2020-04-01 01:14 cc20a865
View on Github →feat(data/nat/basic): simp
lemmas about inequalities with bit*
(#2207)
- feat(data/nat/basic):
simp
lemmas about inequalities withbit*
- Fix compile of
computability/partrec_code
- Fix
nat.bit_cases
to work forType*
too - Generalize some lemmas to
linear_ordered_semiring
s - Apply suggestions from code review Co-Authored-By: Gabriel Ebner gebner@gebner.org
- Apply suggestions from code review Co-Authored-By: Scott Morrison scott@tqft.net
- fixing a proof