div proofs for bitblaster#7

Closed

bollu wants to merge 33 commits intomasterfrom mod-lemmas

+70,086-56,607

Commits on Jun 5, 2024

fix: lake: track trace of cached build logs (leanprover#4343 )
tydeu
authored
fix: missing dsimp simplification when applying auto-congr theorems (leanprover#4352 )
leodemoura
authored
perf: lake: fix LogIO inling/lifting (leanprover#4351 )
tydeu
authored
chore: simplify lean4checker step in release checklist (leanprover#4355 )
kim-em
authored
chore: apply naming convention to IsLawfulSingleton (leanprover#4350 )
leodemoura
authored
fix: split (for if-expressions) should work on non-propositional goals (leanprover#4349 )

leodemoura
and
digama0
authored
doc: add docstrings and examples for String functions (leanprover#4332 )
austinletson
authored
feat: getLsb_signExtend (leanprover#4187 )

authored
chore: use match_expr in omega (leanprover#4358 )
kim-em
authored
fix: GuessLex: delaborate unused parameters as _ (leanprover#4329 )
nomeata
authored
fix: FunInd: support structural recursion on reflexive types (leanprover#4327 )
nomeata
authored
fix: without recover bad simp arg should fail (leanprover#4359 )
nomeata
authored
chore: CI: pr-release: install elan (leanprover#4361 )
nomeata
authored
feat: ppOrigin to use MessageData.ofConst (leanprover#4362 )
nomeata
authored
feat: incrementality for careful command macros such as set_option in theorem, theorem foo.bar, lemma (leanprover#4364 )
Kha
authored
chore: lake: add build log file path to warning (leanprover#4356 )
tydeu
authored
chore: upstream basic String lemmas (leanprover#4354 )
kim-em
authored

Commits on Jun 6, 2024

Commits on Jun 7, 2024

chore: upstream @[simp] attribute (leanprover#4389 )
kim-em
authored

Commits on Jun 8, 2024

chore: start udiv proof
bollu
committed