sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

Commit Graph

  • 2ecd412347 improve consistency Paul Reichert 2026-02-26 16:22:33 +01:00
  • f5c85b698c lemmas Paul Reichert 2026-02-26 14:08:36 +01:00
  • f4e5debf27 wip Paul Reichert 2026-02-26 10:09:00 +01:00
  • f1e7f24a21 remove simp attribute altogether Paul Reichert 2026-02-25 17:42:18 +01:00
  • 26a06e86e1 change simp normal form for List.extract Paul Reichert 2026-02-25 17:24:29 +01:00
  • 9f7df0ef52 cleanups paul/humanevup-33 Paul Reichert 2026-03-09 21:40:56 +01:00
  • 71f51b5a45 cleanups Paul Reichert 2026-03-09 21:32:47 +01:00
  • 8ecd00c9c5 orphan module Paul Reichert 2026-03-01 20:41:13 +01:00
  • a60be4e992 cleanups Paul Reichert 2026-03-01 20:40:33 +01:00
  • a08d5a5f8e add todos Paul Reichert 2026-03-01 19:54:55 +01:00
  • 67c0d1e1e1 cleanups Paul Reichert 2026-03-01 19:53:54 +01:00
  • 75d57290c5 feat: add LawfulDeterministicIterator instances for RxcIterator and RxoIterator Paul Reichert 2026-03-01 18:43:55 +00:00
  • 59036e9442 feat: add getElem?_toArray_stepSize theorem Paul Reichert 2026-03-01 17:35:45 +00:00
  • bb59d9c00f feat: add LawfulDeterministicIterator instances for base iterators and combinators Paul Reichert 2026-03-01 17:00:52 +00:00
  • f6a56da39a help orphan Paul Reichert 2026-03-01 16:57:56 +01:00
  • fa96b5c37e cleanups Paul Reichert 2026-03-01 16:44:25 +01:00
  • 713b8c4bb3 cleanups Paul Reichert 2026-03-01 16:39:31 +01:00
  • 25e12fa62f wip Paul Reichert 2026-03-01 13:58:25 +01:00
  • b877dd6cbf feat: add LawfulDeterministicIterator instance for stepSize iterator Paul Reichert 2026-03-01 00:22:21 +00:00
  • 2d31b9edcf feat: add length_stepSize theorem for stepSize iterator Paul Reichert 2026-02-28 23:56:18 +00:00
  • 448b138174 feat: add stepSize iterator verification lemmas and fix sorry Paul Reichert 2026-02-28 23:04:39 +00:00
  • 40571b00b6 wip Paul Reichert 2026-02-14 21:20:22 +01:00
  • a3be74a90d wip: lemmas about step size iterator Paul Reichert 2026-02-13 20:53:58 +01:00
  • 7190a9d99b cleanups paul/phashmap-iter Paul Reichert 2026-03-09 21:26:05 +01:00
  • 079db91c8c feat: append iterator combinator (#12844) Paul Reichert 2026-03-09 21:22:31 +01:00
  • 007e082b1c feat: bundle leantar with Lean (#12822) Mac Malone 2026-03-09 16:10:59 -04:00
  • cdfde63734 feat: tree map toArray/keysArray lemmas (#12481) Paul Reichert 2026-03-09 21:04:59 +01:00
  • 2e06fb5008 perf: fuse fvar substitution into instantiateMVars (#12233) Joachim Breitner 2026-03-09 18:05:21 +01:00
  • f3b9f37acc refactor: move scopeCacheProofs to tests/elab/ joachim/instantiateMVarsNoUpdate Joachim Breitner 2026-03-09 16:56:24 +00:00
  • 8a05b37758 refactor: rename instantiate_mvars_all.cpp to instantiate_mvars.cpp Joachim Breitner 2026-03-09 16:18:50 +00:00
  • aa6771c8fc refactor: remove redundant instantiateMVars tests Joachim Breitner 2026-03-09 16:05:07 +00:00
  • 37f10435a9 fix: make option linter.unusedSimpArgs respect linter.all (#12560) fiforeach 2026-03-09 16:12:02 +01:00
  • a4dd66df62 perf: bypass typeclass synthesis in SizeOf spec theorem generation (#12849) Joachim Breitner 2026-03-09 16:08:48 +01:00
  • 885266b8f9 refactor: remove unused abstractMVarFVars Joachim Breitner 2026-03-09 15:03:48 +00:00
  • 6ee4d65f13 doc: note that scopeCacheProofs is Claude-generated and removable Joachim Breitner 2026-03-09 14:56:30 +00:00
  • 2c648c7db0 fix: adapt scopeCacheProofs to List.getElem?_inj iff change Joachim Breitner 2026-03-09 14:40:03 +00:00
  • eca4e4112e feat: defeqParam gadget for delayed assignment metavariables Kyle Miller 2026-03-09 07:39:51 -07:00
  • ae45f9e889 tests Paul Reichert 2026-03-09 15:34:16 +01:00
  • dac43d4a7b persistent hash map iterator Paul Reichert 2026-03-09 15:23:20 +01:00
  • 6d24fb2d6a fix: bypass typeclass synthesis in SizeOf spec theorem generation joachim/sizeOfInst Joachim Breitner 2026-03-09 14:20:33 +00:00
  • f5f16abe2e Merge origin/nightly-with-mathlib Joachim Breitner 2026-03-09 14:06:25 +00:00
  • f96d501820 refactor: remove old instantiateMVars and variant entry points Joachim Breitner 2026-03-09 14:06:12 +00:00
  • 40e8f4c5fb chore: turn on new do elaborator in Core (#12656) Sebastian Graf 2026-03-09 20:38:33 +08:00
  • 63098493b3 chore: add --force option to fix_expected.py (#12847) Garmelon 2026-03-09 13:21:04 +01:00
  • fe3ba4dc4c fix: make the omit, unusedSectionVars and loopingSimpArgs linter respect linter.all (#12563) Michael Rothgang 2026-03-09 12:58:02 +01:00
  • 3434c49d02 refactor: remove dead Sort/Const cases from instantiateMVars pass 2 Joachim Breitner 2026-03-09 11:07:02 +00:00
  • 44303c6b2f fix: clamp result_scope after delayed mvar resolution in instantiateMVars Joachim Breitner 2026-03-09 11:01:02 +00:00
  • e9e46f4199 chore: fix two semantic merge errors in SymM mvcgen (#12845) Sebastian Graf 2026-03-09 19:00:01 +08:00
  • eba487b7c2 chore: fix two semantic merge errors in SymM mvcgen sg/mvcgen-errors Sebastian Graf 2026-03-09 10:50:23 +00:00
  • 8714dd7aff fix: use map_reuse for levels in instantiateMVars pass 1 Joachim Breitner 2026-03-09 10:30:16 +00:00
  • 6451b94095 append iterator paul/iter-append Paul Reichert 2026-03-09 11:10:13 +01:00
  • f37049a6c1 refactor: move instantiate_mvars_all and scope_cache to library Joachim Breitner 2026-03-09 09:53:34 +00:00
  • b84de014bf fix: preserve application prefix sharing in instantiateMVars Joachim Breitner 2026-03-09 09:48:48 +00:00
  • e2b500b204 chore: update stage0 Lean stage0 autoupdater 2026-03-09 08:53:25 +00:00
  • f9aeed3d40 perf: fix quadratic scaling in unused variable linter joachim/bench-linter-fix Joachim Breitner 2026-03-09 08:28:32 +00:00
  • e804829101 feat: have #eval elaborate variables (#11427) Kyle Miller 2026-03-08 21:52:08 -07:00
  • 27b583d304 feat: mutually dependent structure default values, and avoiding self-dependence (#12841) Kyle Miller 2026-03-08 21:15:06 -07:00
  • d8accf47b3 chore: use terminology "non-recursive structure" instead of "struct-like" (#12749) Kyle Miller 2026-03-08 20:44:38 -07:00
  • ad8fa9c419 remove cycle check kmill_structure_mutual_defaults Kyle Miller 2026-03-08 16:12:04 -07:00
  • 32be33be06 remove dependencies from local context Kyle Miller 2026-03-08 16:05:55 -07:00
  • 4068ce0f9e feat: prove interpreter soundness for Radix DSL radix/examples Leonardo de Moura 2026-03-08 23:01:05 +00:00
  • 9097bcbe34 feat: prove interpreter correctness for Radix DSL Leonardo de Moura 2026-03-08 22:20:52 +00:00
  • 3cfaf24e92 fix: resolve build errors in Radix DSL Leonardo de Moura 2026-03-08 18:51:55 +00:00
  • 7afdd76d94 doc: update radix-plan with completed proofs and zero sorry Leonardo de Moura 2026-03-08 16:18:58 +00:00
  • a51c0e0544 chore: remove tracked .olean files from Radix Leonardo de Moura 2026-03-08 16:16:35 +00:00
  • 0feeb6b31f feat: prove callStmt soundness by adding WellTypedFuns hypothesis Leonardo de Moura 2026-03-08 16:10:17 +00:00
  • fea941817d feat: mutually dependent structure default values, and self-dependence checking Kyle Miller 2026-03-08 12:44:28 -07:00
  • 020e918b1c feat: add linear ownership typing with soundness proof for Radix DSL Leonardo de Moura 2026-03-08 13:52:01 +00:00
  • bfef80c9e3 feat: extend DSL syntax with let, alloc, free, array ops Leonardo de Moura 2026-03-08 02:33:12 +00:00
  • 9d1dc208bd feat: add executable examples (factorial, fibonacci, collatz, fizzbuzz, bubble sort) Leonardo de Moura 2026-03-08 02:06:19 +00:00
  • 96f28d046d feat: complete type safety preservation with zero sorry Leonardo de Moura 2026-03-08 01:55:58 +00:00
  • fb86c4e457 doc: add Radix project plan overview for sharing Leonardo de Moura 2026-03-08 01:43:37 +00:00
  • 0dfee989a8 test: add 63 tests covering edge cases, scope, optimizations, and errors Leonardo de Moura 2026-03-08 01:34:21 +00:00
  • 346d35a306 doc: add module docstrings and definition documentation across Radix DSL Leonardo de Moura 2026-03-08 01:34:11 +00:00
  • 80ecb30c2b Merge pull request #35 from leodemoura/radix/remove-partial-prove-correctness Leonardo de Moura 2026-03-07 17:18:35 -08:00
  • 289c099bf5 chore: add lakefile.toml for Radix DSL project Leonardo de Moura 2026-03-08 01:17:57 +00:00
  • 19a8e575f7 feat: prove inline correctness by adding Stmt.scope for frame isolation Leonardo de Moura 2026-03-08 01:07:14 +00:00
  • 924068293c Merge pull request #33 from leodemoura/radix/remove-partial-prove-correctness Leonardo de Moura 2026-03-07 16:02:39 -08:00
  • fe47556d24 feat: prove 6/7 type preservation cases for Radix DSL Leonardo de Moura 2026-03-07 23:41:28 +00:00
  • 01bfa5936a feat: remove Expr.call, prove ConstProp, make inline total Leonardo de Moura 2026-03-07 22:43:09 +00:00
  • 68da7aa864 feat: prove copy propagation correctness, restore typed identity simplifications Leonardo de Moura 2026-03-07 22:23:28 +00:00
  • df0b56be68 feat: remove partial, fix interpreter ret, prove optimization correctness Leonardo de Moura 2026-03-07 21:48:20 +00:00
  • 38f554486c Merge pull request #27 from leodemoura/radix/initial-implementation Leonardo de Moura 2026-03-07 12:25:25 -08:00
  • 58dc3a7739 feat: add Radix embedded DSL with semantics, optimizations, and proofs Leonardo de Moura 2026-03-07 20:24:01 +00:00
  • 74d90c81d4 test: complete scope_cache formal verification Joachim Breitner 2026-03-07 20:17:32 +00:00
  • f82aa9aedf refactor: path compression for DiscrTree joachim/compress-discrtree Joachim Breitner 2026-03-07 16:07:35 +00:00
  • 530842e843 feat: lake: inherit restoreAllArtifacts from workspace (#12837) Mac Malone 2026-03-06 22:34:25 -05:00
  • 9c852d2f8c fix: lake: emit .nobuild trace only if .trace exists (#12835) Mac Malone 2026-03-06 20:25:28 -05:00
  • 387a975099 feat: use precise instance tracking for grind.unusedLemmaThreshold Kim Morrison 2026-03-07 01:03:14 +00:00
  • 00659f8e60 chore: make fsanitize CI non-blocking for releases v4.29.0-rc6 Kim Morrison 2026-03-07 00:48:51 +00:00
  • 68e280cda0 fix: address shellcheck SC2129 by grouping redirects Kim Morrison 2026-03-07 00:19:55 +00:00
  • ee4153eb65 feat(ci): add lake-ci label to enable full Lake test suite Kim Morrison 2026-03-07 00:16:19 +00:00
  • 54c17a822e Merge remote-tracking branch 'origin/master' into lake-profile lake-profile Kim Morrison 2026-03-07 00:17:21 +00:00
  • c948d24b6d chore: update stage0 Lean stage0 autoupdater 2026-03-07 00:02:16 +00:00
  • da0bdb2e07 fix: remove unused simp argument LE.ofLT in Order.Factories Kim Morrison 2026-03-06 23:22:48 +00:00
  • c1bcc4d1ac fix: address unused simp theorem warnings (#12829) Paul Reichert 2026-03-07 00:12:03 +01:00
  • a69f282f64 feat: add openssl to the guide sofia/openssl Sofia Rodrigues 2026-03-06 19:34:10 -03:00
  • bb745f8b7c feat: openssl nix Sofia Rodrigues 2026-01-16 19:04:34 -03:00
  • 33afc77402 fix: remove tls Sofia Rodrigues 2026-01-16 18:54:46 -03:00
  • 07f15babe3 feat: start openssl Sofia Rodrigues 2026-01-15 16:10:09 -03:00