feat: add `Bitvec.toFin_twoPow`#51

Closed

luisacicolini wants to merge 419 commits intomasterfrom

twopow-tofin

This pull request is big! We're only showing the most recent 250 commits

Commits on Feb 25, 2025

chore: CI: bump dawidd6/action-download-artifact from 7 to 8 (#6903)

dependabot[bot]
authored and
luisacicolini
committed
feat: align List/Array/Vector.insertIdx lemmas (#6948)

kim-em
authored and
luisacicolini
committed
chore: re-land "perf: use C23's `free_sized` when available" (#6844)

eric-wieser
authored and
luisacicolini
committed
feat: add `BitVec.(getMsbD, msb)_replicate, replicate_one` (#6326)

luisacicolini
and
alexkeizer
committed
fix: make `rewrite`/`rw` tactic abort on elaboration errors (#6891)

kmill
authored and
luisacicolini
committed
feat: add `Hashable` instances for `PUnit` and `PEmpty` (#6866)

javra
authored and
luisacicolini
committed
feat: improve simp trace formatting (#6951)

nomeata
authored and
luisacicolini
committed
feat: add `BitVec.(getElem_umod_of_lt, getElem_umod, getLsbD_umod, getMsbD_umod)` (#6795)

luisacicolini
and
bollu
committed
feat: allow anonymous equality proofs in `match` expressions (#6853)

jrr6
authored and
luisacicolini
committed
feat: inlay hints for auto-implicits (#6768)

mhuisi
authored and
luisacicolini
committed
chore: update stage0

Lean stage0 autoupdater
authored and
luisacicolini
committed
chore: restore example after stage0 update (#6942)

zwarich
authored and
luisacicolini
committed
test: more equational theorem generation tests (#6952)

nomeata
authored and
luisacicolini
committed
feat: frontend & server support for plugins (#6893)

tydeu
authored and
luisacicolini
committed
fix: show error messages on name conflicts in `mutual` blocks (#6939)

jrr6
authored and
luisacicolini
committed
feat: add SMT-LIB overflow on addition for bitvectors `BitVec.(uadd_overflow, sadd_overflow, uadd_overflow_eq, sadd_overflow_eq)` and support theorems (#6628)

committed
chore: fix variable names in List lemmas (#6953)

kim-em
authored and
luisacicolini
committed
feat: add `auto_attach` simp set (no functionality yet) (#6956)

nomeata
authored and
luisacicolini
committed
chore: update stage0

Lean stage0 autoupdater
authored and
luisacicolini
committed
feat: allow updating binders to and from strict- and instance-implicit (#6634)

jrr6
authored and
luisacicolini
committed
chore: update stage0

Lean stage0 autoupdater
authored and
luisacicolini
committed
feat: `evalAndSuggest` helper tactic (#6961)

leodemoura
authored and
luisacicolini
committed
doc: improve List.toArray doc-string (#6962)

kim-em
authored and
luisacicolini
committed
chore: further cleanup of index variable naming in List (#6963)

kim-em
authored and
luisacicolini
committed
feat: `#info_trees in` command (#6964)

kim-em
authored and
luisacicolini
committed
feat: implement `try?` using `evalAndSuggest` (#6965)

leodemoura
authored and
luisacicolini
committed
feat: add internal linter for List/Array/Vector variable names (#6966)

kim-em
authored and
luisacicolini
committed
feat: use `expose_names` in `try?` (#6967)

leodemoura
authored and
luisacicolini
committed
chore: update stage0

Lean stage0 autoupdater
authored and
luisacicolini
committed
doc: style guide and naming convention for the standard library (#6950)

TwoFX
authored and
luisacicolini
committed
chore: rename Nat.not_eq_zero_of_lt (#6968)

kim-em
authored and
luisacicolini
committed
feat: binderNameHint (#6947)

nomeata
authored and
luisacicolini
committed
refactor: bv_decide's type analysis to prepare for enum support (#6971)

hargoniX
authored and
luisacicolini
committed
refactor: rename auto_attach attribute to wf_preprocess (#6972)

nomeata
authored and
luisacicolini
committed
chore: update stage0

Lean stage0 autoupdater
authored and
luisacicolini
committed
feat: inlay hint refinements (#6959)

mhuisi
authored and
luisacicolini
committed
chore: update stage0

Lean stage0 autoupdater
authored and
luisacicolini
committed
fix: inlay hints in untitled files (#6978)

mhuisi
authored and
luisacicolini
committed
feat: `try?` composite suggestions (#6979)

leodemoura
authored and
luisacicolini
committed
feat: improve some files separation and standardize error messages in UV modules (#6830)

algebraic-dev
authored and
luisacicolini
committed
feat: `try?` validation and cleanup (#6980)

leodemoura
authored and
luisacicolini
committed
feat: `try?` tactic improvements (#6981)

leodemoura
authored and
luisacicolini
committed
chore: linting List (#6970)

kim-em
authored and
luisacicolini
committed
feat: improve monadic Array lemmas (#6982)

kim-em
authored and
luisacicolini
committed
feat: respect `Task.map/bind (sync := true)` after waiting (#6976)

Kha
authored and
luisacicolini
committed
perf: avoid taking mutex on already-resolved promises (#6984)

Kha
authored and
luisacicolini
committed
feat: API to avoid deadlocks from dropped promises (#6958)

Kha
authored and
luisacicolini
committed
fix: convert kernel interrupt into elab interrupt (#6988)

Kha
authored and
luisacicolini
committed
chore: re-enable `Elab.async` in the server (#6990)

Kha
authored and
luisacicolini
committed
feat: improve `try?` suggestion (#6991)

leodemoura
authored and
luisacicolini
committed
feat: parallel progress notifications (#6329)

Kha
authored and
luisacicolini
committed
chore: disable broken test

leodemoura
authored and
luisacicolini
committed
feat: compress `try?` suggestions (#6994)

leodemoura
authored and
luisacicolini
committed
feat: `exact?` in `try?` (#6995)

leodemoura
authored and
luisacicolini
committed
refactor: elaborate forIn notation without extra let (#6977)

nomeata
authored and
luisacicolini
committed
chore: change Lake configuration error message (#6829)

BoltonBailey
authored and
luisacicolini
committed
doc: mention `Prop`s are equal to `True` or `False` (#6998)

kmill
authored and
luisacicolini
committed
feat: add `Int.Linear` normalization support (#7000)

leodemoura
authored and
luisacicolini
committed
feat: linear integer arith normalizer (#7002)

leodemoura
authored and
luisacicolini
committed
chore: remove unused Int simp lemmas (#7005)

kim-em
authored and
luisacicolini
committed
feat: `bv_decide` hint (#7009)

leodemoura
authored and
luisacicolini
committed
chore: improve `expose_names` doc string (#7010)

leodemoura
authored and
luisacicolini
committed
feat: `simp +arith` for integers (#7011)

leodemoura
authored and
luisacicolini
committed
chore: improve `withAbstractAtoms` (#7012)

leodemoura
authored and
luisacicolini
committed
chore: unprotect List.foldlM (#7003)

kim-em
authored and
luisacicolini
committed
feat: `simp +arith` normalizes coefficient in linear integer polynomials (#7015)

leodemoura
authored and
luisacicolini
committed
feat: basic support for handling enum inductives in bv_decide (#6946)

hargoniX
authored and
luisacicolini
committed
chore: add @[simp] to List.flatten_toArray (#7014)

kim-em
authored and
luisacicolini
committed
chore: replace HashMap.get_ lemmas with getElem_ versions (#7004)

kim-em
authored and
luisacicolini
committed
chore: rename simp sets (#7018)

kim-em
authored and
luisacicolini
committed
chore: `Task.get` block profiling (#7016)

Kha
authored and
luisacicolini
committed
chore: update stage0

Lean stage0 autoupdater
authored and
luisacicolini
committed
fix: correct trace nodes in bv_decide (#7019)

hargoniX
authored and
luisacicolini
committed
feat: improvements to simp confluence (#7013)

kim-em
authored and
luisacicolini
committed
feat: add basic extract theorems for bv_decide (#7021)

hargoniX
authored and
luisacicolini
committed
chore: deprecated compile_time_search_path% (#7022)

kim-em
authored and
luisacicolini
committed
chore: rename simp sets (#7017)

kim-em
authored and
luisacicolini
committed
fix: codegen was allowed improper env ext accesses (#7023)

Kha
authored and
luisacicolini
committed
doc: misc. style guide and naming scheme additions (#7026)

TwoFX
authored and
luisacicolini
committed
chore: update stage0

Lean stage0 autoupdater
authored and
luisacicolini
committed
feat: nested well-founded recursion via automatic preprocessing (#6744)

nomeata
authored and
luisacicolini
committed
chore: trivial changes from async-proofs branch (#7028)

Kha
authored and
luisacicolini
committed
feat: bv_decide rewrite multiplication with power of two to shift (#7029)

hargoniX
authored and
luisacicolini
committed
chore: build Lean with `Elab.async` (#6989)

Kha
authored and
luisacicolini
committed
feat: lake: provide help on Elan's `+` option (#7024)

tydeu
authored and
luisacicolini
committed
feat: linear integer inequality normalization using `gcd` of coefficients (#7030)

leodemoura
authored and
luisacicolini
committed
feat: present bv_decide counter examples for UIntX and enums better (#7033)

hargoniX
authored and
luisacicolini
committed
feat: tree map data structures and operations (#6914)

datokrat
authored and
luisacicolini
committed
feat: `simp +arith` sorts linear atoms (#7040)

leodemoura
authored and
luisacicolini
committed
chore: remove dead code from `Nat/Linear.lean` (#7042)

leodemoura
authored and
luisacicolini
committed
chore: `simp_arith` has been deprecated (#7043)

leodemoura
authored and
luisacicolini
committed
chore: fix `linter.listVariables` naming (#7044)

kim-em
authored and
luisacicolini
committed
chore: update stage0

Lean stage0 autoupdater
authored and
luisacicolini
committed
test: fix `simp_arith1` benchmark (#7049)

Kha
authored and
luisacicolini
committed
feat: wf_preprocess for {List,Array}.Monadic functions (#7034)

nomeata
authored and
luisacicolini
committed
fix: make several LCNF environment extensions have asyncMode of .sync (#7041)

zwarich
authored and
luisacicolini
committed
chore: remove `save` tactic (#7047)

Kha
authored and
luisacicolini
committed
chore: compile against glibc 2.26 (#7037)

Kha
authored and
luisacicolini
committed
feat: propagate wfParam through let (#7039)

nomeata
authored and
luisacicolini
committed
feat: `IntX.ofBitVec` (#7048)

TwoFX
authored and
luisacicolini
committed
chore: add `UIntX.ofNatLT` (#7057)

TwoFX
authored and
luisacicolini
committed
chore: rename `UIntX.mk` -> `UIntX.ofBitVec` (#7046)

TwoFX
authored and
luisacicolini
committed
chore: update stage0

Lean stage0 autoupdater
authored and
luisacicolini
committed
refactor: move `grind` offset constraint module to `Grind/Arith/Offset` (#7058)

leodemoura
authored and
luisacicolini
committed
chore: upstream an Int lemma (#7060)

kim-em
authored and
luisacicolini
committed
chore: rename `UIntX.val` -> `UIntX.toFin` (#7050)

TwoFX
authored and
luisacicolini
committed
feat: `UIntX.ofFin` (#7056)

TwoFX
authored and
luisacicolini
committed
feat: binderNameHint in congr (#7053)

nomeata
authored and
luisacicolini
committed
feat: missing conversion functions for `ISize` (#7063)

TwoFX
authored and
luisacicolini
committed
feat: deprecated find, fold, foldM, mergeBy functions for the tree map (#7036)

datokrat
authored and
luisacicolini
committed
chore: make `IntX` constructor private, provide `UIntX.toIntX` (#7062)

TwoFX
authored and
luisacicolini
committed
chore: rename `IntX.toNat` -> `IntX.toNatClampNeg` (#7066)

TwoFX
authored and
luisacicolini
committed
chore: rename `BitVec.ofNatLt` -> `BitVec.ofNatLT` (#7064)

TwoFX
authored and
luisacicolini
committed
doc: fix typo (#7067)

chabulhwi
authored and
luisacicolini
committed
chore: dsimproc for UIntX.ofNatLT (#7068)

TwoFX
authored and
luisacicolini
committed
chore: update stage0

Lean stage0 autoupdater
authored and
luisacicolini
committed
feat: premise selection API (#7061)

kim-em
authored and
luisacicolini
committed
feat: support theorems for cutsat `Div-Solve` rule (#7077)

leodemoura
authored and
luisacicolini
committed
feat: lake: support plugins (#7001)

tydeu
authored and
luisacicolini
committed
feat: simprocs for `Int` and `Nat` divides predicates (#7078)

leodemoura
authored and
luisacicolini
committed
chore: rename `UIntX.ofNatCore`, `UIntX.ofNat'` -> `UIntX.ofNatLT` (#7071)

TwoFX
authored and
luisacicolini
committed
feat: insertMany, ofList, ofArray, foldr, foldM functions for the tree map (#7051)

datokrat
authored and
luisacicolini
committed
fix: incremental goal state requests select incomplete snapshot (#6887)

mhuisi
authored and
luisacicolini
committed
feat: request cancellation (#7054)

mhuisi
authored and
luisacicolini
committed
feat: `IntX.minValue`, `IntX.maxValue`, `IntX.ofIntLE`, `IntX.ofIntTruncate` (#7081)

TwoFX
authored and
luisacicolini
committed
feat: `UIntX.ofNatTruncate` (#7080)

TwoFX
authored and
luisacicolini
committed
feat: `Fin.toNat` (#7079)

TwoFX
authored and
luisacicolini
committed
feat: make binders in `#check` be hoverable (#7074)

kmill
authored and
luisacicolini
committed
feat: add helper theorems for normalizing divisibility constraints (#7091)

leodemoura
authored and
luisacicolini
committed
fix: ensure `get_elem_tactic` works in absence of goals (#7088)

jrr6
authored and
luisacicolini
committed
feat: divisibility constraint normalizer (#7092)

leodemoura
authored and
luisacicolini
committed
refactor: `Int.Linear` module (#7093)

leodemoura
authored and
luisacicolini
committed
refactor: add `denote'` functions to `Int/Linear.lean` (#7094)

leodemoura
authored and
luisacicolini
committed
chore: cleanup and missing `grind` normalization rules (#7095)

leodemoura
authored and
luisacicolini
committed
feat: make `BitVec.getElem` the simp normal form and use it in `ext` (#5498)

authored and
luisacicolini
committed
feat: cutsat preparations (#7097)

leodemoura
authored and
luisacicolini
committed
feat: cutsat helper functions (#7098)

leodemoura
authored and
luisacicolini
committed
feat: fun_induction and fun_cases tactics (#7069)

nomeata
authored and
luisacicolini
committed
fix: allow trailing comma in array syntax (#7055)

Seasawher
authored and
luisacicolini
committed
fix: `grind` using `reducible` transparency setting (#7102)

leodemoura
authored and
luisacicolini
committed
feat: cleanup of `get` and `back` functions on `List`/`Array` (#7059)

kim-em
authored and
luisacicolini
committed
feat: add `BitVec.[(getMsbD, msb)_extractLsb', (getLsbD, getMsbD, msb)_extractLsb] `, add `and_eq_decide, or_eq_decide, decide_eq_true_iff` to `bool_to_prop ` (#6792)

committed
feat: align Array/Vector.extract lemmas with List (#7105)

kim-em
authored and
luisacicolini
committed
feat: complete aligning List/Array/Vector.finRange (#7106)

kim-em
authored and
luisacicolini
committed
feat: tree map lemmas about empty, isEmpty, insert, contains (#6850)

datokrat
authored and
luisacicolini
committed
fix: race condition led to `(sync := true)` tasks being spawned as separate dedicated tasks (#7089)

Kha
authored and
luisacicolini
committed
doc: style guide additions (#7111)

TwoFX
authored and
luisacicolini
committed
feat: min, max, minKey, maxKey, atIndex, getEntryLE, getKeyLE, ... functions for the tree map (#7070)

datokrat
authored and
luisacicolini
committed
chore: linting variable names for List (#7107)

kim-em
authored and
luisacicolini
committed
feat: auto-implicit inlay hint tooltip & instance inlay hints (#7112)

mhuisi
authored and
luisacicolini
committed
feat: conversions between `Float` and finite integers (#7083)

TwoFX
authored and
luisacicolini
committed
feat: values and valuesArray functions for the tree map (#7114)

datokrat
authored and
luisacicolini
committed
fix: FunInd to clear match discriminants if possible

nomeata
authored and
luisacicolini
committed
chore: update stage0

nomeata
authored and
luisacicolini
committed
chore: update code after #7110

nomeata
authored and
luisacicolini
committed
chore: cleanup duplicate theorems (#7113)

kim-em
authored and
luisacicolini
committed
chore: repair defeqs for List GetElem instances (#7121)

kim-em
authored and
luisacicolini
committed
feat: add divisibility constraint solver to `grind` (#7122)

leodemoura
authored and
luisacicolini
committed
chore: make internal List getters private (#7123)

kim-em
authored and
luisacicolini
committed
feat: add generalization hypotheses to `induction` tactic (#7103)

kmill
authored and
luisacicolini
committed
chore: update stage0

Lean stage0 autoupdater
authored and
luisacicolini
committed
feat: cutsat divisibility constraint solver proof by reflection theorems (#7124)

leodemoura
authored and
luisacicolini
committed
chore: cleanup after stage0 update for #7103 (#7125)

kmill
authored and
luisacicolini
committed
feat: make structure parent projections nameable (#7100)

kmill
authored and
luisacicolini
committed
feat: make linter names clickable in trace messages (#7119)

eric-wieser
authored and
luisacicolini
committed
feat: getThenInsertIfNew? and partition functions for the tree map (#7109)

datokrat
authored and
luisacicolini
committed
feat: getKey functions for the tree map (#7116)

datokrat
authored and
luisacicolini
committed
chore: remove semantic highlighting timeout (#7130)

mhuisi
authored and
luisacicolini
committed
feat: `Repr` and `Hashable` for `IntX` (#7128)

TwoFX
authored and
luisacicolini
committed
fix: fun_induction to generalize like induction does (#7127)

nomeata
authored and
luisacicolini
committed
chore: update stage0

Lean stage0 autoupdater
authored and
luisacicolini
committed
feat: `fun_induction foo` (no arguments) (#7101)

nomeata
authored and
luisacicolini
committed
feat: verify `toList` for hash maps (#6954)

jt0202
authored and
luisacicolini
committed
feat: `IntX.abs` (#7131)

TwoFX
authored and
luisacicolini
committed
chore: review uses of `generalize` (#7126)

kmill
authored and
luisacicolini
committed
feat: try? to use fun_induction (#7082)

nomeata
authored and
luisacicolini
committed
chore: add Array.getInternal, also @[extern]

kim-em
authored and
luisacicolini
committed
chore: update stage0

kim-em
authored and
luisacicolini
committed
chore: use as[i] instead of as.get i

kim-em
authored and
luisacicolini
committed
chore: deprecate Array.get

kim-em
authored and
luisacicolini
committed
feat: proof production for divisibility constraint solver in `grind` (#7138)

leodemoura
authored and
luisacicolini
committed
feat: smarter plugin loading (#7090)

tydeu
authored and
luisacicolini
committed
feat: create a `let`-expression for storing the context in `cutsat` proofs (#7139)

leodemoura
authored and
luisacicolini
committed
feat: faster auto-completion (#7134)

mhuisi
authored and
luisacicolini
committed
test: add f91 definition using partial_fixpoint (#7144)

nomeata
authored and
luisacicolini
committed
chore: update stage0

Lean stage0 autoupdater
authored and
luisacicolini
committed
chore: linting variable names in List/Array (#7146)

kim-em
authored and
luisacicolini
committed
feat: FunInd to split on bif as well

nomeata
authored and
luisacicolini
committed
chore: update stage0

nomeata
authored and
luisacicolini
committed
refactor: update proofs after stage0 update for #7140

nomeata
authored and
luisacicolini
committed
refactor: use more fun_induction in Init.Data.Int.Linear (#7142)

nomeata
authored and
luisacicolini
committed
feat: infrastructure for inequalities constraints in cutsat (#7152)

leodemoura
authored and
luisacicolini
committed
chore: complete variable name linting for Vector (#7154)

kim-em
authored and
luisacicolini
committed
feat: model search skeleton for `cutsat` (#7155)

leodemoura
authored and
luisacicolini
committed
feat: helper theorem for cutsat (#7156)

leodemoura
authored and
luisacicolini
committed
feat: strengthen Int.tdiv_eq_ediv (#7158)

kim-em
authored and
luisacicolini
committed
feat: fast path for inlay hints (#7149)

mhuisi
authored and
luisacicolini
committed
feat: modify and alter functions for the tree map (#7118)

datokrat
authored and
luisacicolini
committed
feat: more robust server parallelism (#7087)

mhuisi
authored and
luisacicolini
committed
chore: split Int.DivModLemmas into Bootstrap and Lemmas (#7162)

kim-em
authored and
luisacicolini
committed
fix: inlay hint assertion violation (#7164)

mhuisi
authored and
luisacicolini
committed
feat: more tree map lemmas about empty, isEmpty, contains, size, insert, erase (#7161)

datokrat
authored and
luisacicolini
committed
feat: upgrade Int.tdiv_eq_ediv to an unconditional equivalence (#7163)

kim-em
authored and
luisacicolini
committed
feat: staged CMake build with Lake as a plugin (#6929)

tydeu
authored and
luisacicolini
committed
feat: run `setup-file` on lakefiles (#7153)

tydeu
authored and
luisacicolini
committed
feat: use Lake plugin for Lake imports (#7157)

tydeu
authored and
luisacicolini
committed
feat: `Elab.Deriving` trace on `applyDerivingHandlers` (#7173)

Kha
authored and
luisacicolini
committed
feat: verify fold/for variants for Hashmaps (#7137)

authored and
luisacicolini
committed
feat: model construction for divisibility constraints in cutsat (#7176)

leodemoura
authored and
luisacicolini
committed
fix: do not cancel async elaboration tasks (#7175)

Kha
authored and
luisacicolini
committed
feat: improve cutsat model search procedure (#7183)

leodemoura
authored and
luisacicolini
committed
fix: lake: `setup-file` on an invalid Lean config (#7182)

tydeu
authored and
luisacicolini
committed
test: avoid re-elaboration of interactive runner (#7177)

Kha
authored and
luisacicolini
committed
feat: support LEAN_BACKTRACE on macOS (#7184)

zwarich
authored and
luisacicolini
committed
fix: inlay hint race conditions (#7188)

mhuisi
authored and
luisacicolini
committed
perf: optimize `sorry` detection in unused variables linter (#7129)

Kha
authored and
luisacicolini
committed
chore: don't forget about namespace reservation for async-unsupported constant kinds (#6987)

Kha
authored and
luisacicolini
committed
refactor: cutsat (#7186)

leodemoura
authored and
luisacicolini
committed
chore: cutsat cleanup (#7189)

leodemoura
authored and
luisacicolini
committed
chore: cutsat equality infrastructure (#7193)

leodemoura
authored and
luisacicolini
committed
feat: helper theorems for solving equality in cutsat (#7194)

leodemoura
authored and
luisacicolini
committed
feat: `simp` diagnostics in `grind` (#6902)

leodemoura
authored and
luisacicolini
committed
doc: remove Trepplein example (Lean 3) (#7197)

euprunin
authored and
luisacicolini
committed
chore: post-#7100 cleanup (#7196)

kmill
authored and
luisacicolini
committed
chore: additional newline before 'additional diagnostic information' message (#7169)

kim-em
authored and
luisacicolini
committed
feat: complete comparison theorems for `ediv/tdiv/fdiv` and `emod/tmod/fmod` (#7199)

kim-em
authored and
luisacicolini
committed
feat: align List/Array/Vector.leftpad (#7201)

kim-em
authored and
luisacicolini
committed
feat: cutsat relevant-term internalization (#7202)

leodemoura
authored and
luisacicolini
committed
feat: improve support for equations in cutsat (#7203)

leodemoura
authored and
luisacicolini
committed
feat: allow line-wrapping when printing `DiscrTree.Key`s (#7200)

eric-wieser
authored and
luisacicolini
committed
feat: tree map lemmas about containsThenInsert(IfNew) (#7165)

datokrat
authored and
luisacicolini
committed
feat: align lemmas about List.getLast(!?) with Array/Vector.back(!?) (#7205)

kim-em
authored and
luisacicolini
committed
feat: `UIntX` conversion lemmas (part 1/n) (#7174)

TwoFX
authored and
luisacicolini
committed
feat: TreeMap lemmas for 'get?' (#7167)

datokrat
authored and
luisacicolini
committed
feat: add `BitVec.toFin_abs` (#7206)

luisacicolini
and
tobiasgrosser
committed
fix: lake: MSYS2 `OSTYPE` change (#7209)

tydeu
authored and
luisacicolini
committed
chore: use getElem in RHS of getElem theorems (#7187)

tobiasgrosser
authored and
luisacicolini
committed
feat: add `ForIn` instance for `PHashSet` (#7214)

leodemoura
authored and
luisacicolini
committed
chore: re-enable List variable linter (#7215)

kim-em
authored and
luisacicolini
committed
feat: improve equality support in cutsat (#7217)

leodemoura
authored and
luisacicolini
committed
chore: align List.dropLast/Array.pop lemmas (#7208)

kim-em
authored and
luisacicolini
committed
chore: List.leftpad typo (#7219)

kim-em
authored and
luisacicolini
committed
feat: missing cases for equality propagation from core to cutsat (#7220)

leodemoura
authored and
luisacicolini
committed
feat: lake: compute jobs asynchronously (#7211)

tydeu
authored and
luisacicolini
committed
fix: make the stage2 Leanc build use stage2 oleans rather than stage1 oleans (#7190)

zwarich
authored and
luisacicolini
committed
chore: update stage0

Lean stage0 autoupdater
authored and
luisacicolini
committed
fix: replace the `compare_self` simp lemma with a less generic one (#7222)

datokrat
authored and
luisacicolini
committed
chore: old proof with correct simp set
luisacicolini
committed
chore: correct simp lemmas
luisacicolini
committed
chore: fix simp lemmas
luisacicolini
committed