max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean/run
History
Siddharth 4e83f23955
feat: bv_normalize pass: AC normalization of multiplication (#7461) 
This PR introduces a bitvector associativity/commutativity normalization
on bitvector terms of the form `(a * b) = (c * d)` for `a, b, c, d`
bitvectors. This mirrors Bitwuzla's `PassNormalize::process`'s
`PassNormalize::normalize_eq_add_mul`.

For example, `x₁ * (y₁ * z) = x₂ * (y₂ * z)` is normalized to `z * (x₁ *
y₁) = z * (x₂ * y₂)`,
pulling the shared variable `z` to the front on both sides. The PR also
replaces the use of `ac_nf` in the normalization pass of `bv_decide`.

Note that this is based on Bitwuzla's normalizer, and we eventually want
to have support for bitvector addition normalization as well. However,
since we currently lack a `ring` equivalent for bitvectors, we cannot
currently justify rewrites such as `x + x + x → 3 * x`. Similarly, we
leave the implementation of `PassNormalize::normalize_comm_assoc`, which
is called when the toplevel terms are different for a subsequent patch.

For posterity, we record the precise location in Bitwuzla where the
implemented codepath occurs:
```cpp
-- d1f1bc2ad3/src/preprocess/pass/normalize.cpp (L1550-L1554)
        Kind k = cur.kind();
        if (k == Kind::EQUAL && children[0].kind() == children[1].kind()
            && (children[0].kind() == Kind::BV_ADD
                || children[0].kind() == Kind::BV_MUL))
        {
          auto [res, norm] = normalize_eq_add_mul(children[0], children[1]);
          ...
```

---------

Co-authored-by: Henrik Böving <hargonix@gmail.com>
Co-authored-by: Tobias Grosser <github@grosser.es>
2025-03-18 08:28:35 +00:00
..
.gitattributes
.gitignore
28.lean
29.lean
34.lean
52_lean3.lean
91_lean3.lean
102_lean3.lean
108.lean
111.lean
121.lean
125.lean
175.lean
229.lean
262.lean
269.lean
270.lean
280.lean
281.lean
282.lean
303.lean
305.lean
310.lean
319.lean
326.lean
327.lean
329.lean
335.lean
337.lean
338.lean
341.lean
343.lean
345.lean chore: reimplement mk_projections in Lean (#7295) 2025-03-03 01:10:27 +00:00
382.lean
387.lean
394.lean
436.lean
436_lean3.lean
439.lean
441.lean
447_lean3.lean
452.lean
456.lean
457.lean
461a.lean
461b.lean
462.lean
463.lean
470_lean3.lean
471.lean
474_lean3.lean
481.lean
482.lean
492.lean
492_lean3.lean
498.lean
500_lean3.lean
501.lean
509.lean
536.lean
561.lean
569.lean
602.lean
616.lean
633.lean
644.lean
646.lean
654.lean
664.lean
677.lean
696.lean feat: improve letIdLhs parser 2021-09-28 18:10:25 -07:00
716.lean
753.lean
760.lean
764.lean
783.lean
788.lean
790.lean feat: improve simp trace formatting (#6951) 2025-02-04 15:47:01 +00:00
793.lean
796.lean
815.lean
821.lean
837.lean
847.lean
854.lean
860.lean
879.lean
891.lean
909.lean
944.lean fix: ilean loading performance (#4900) 2024-08-29 11:51:48 +00:00
945.lean
946.lean
955.lean
968.lean
972.lean
974.lean
983.lean
986.lean chore: linting variable names in List/Array (#7146) 2025-02-19 12:45:02 +00:00
988.lean
998.lean fix: move auxDeclToFullName to LocalContext to fix name (un)resolution (#7075) 2025-03-03 16:10:54 +00:00
998Export.lean fix: report replay kernel errors as standard diagnostics (#7471) 2025-03-13 18:45:46 +00:00
1016.lean
1017.lean
1018.lean
1020.lean
1022.lean
1024.lean
1025.lean
1026.lean
1029.lean
1030.lean
1037.lean
1051.lean
1058.lean
1074a.lean
1080.lean
1113b.lean
1118.lean
1120.lean
1123.lean
1124.lean
1127.lean
1132.lean
1143.lean
1155.lean
1156.lean chore: use #guard_msgs in run tests (#4175) 2024-05-16 00:38:31 +00:00
1158.lean
1163.lean chore: additional newline before 'additional diagnostic information' message (#7169) 2025-02-23 23:27:33 +00:00
1168.lean
1169.lean
1171.lean
1179b.lean
1182.lean
1184.lean
1192.lean
1193a.lean
1193b.lean
1194.lean
1200.lean
1202.lean
1224.lean
1228.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
1230.lean
1234.lean feat: improve simp trace formatting (#6951) 2025-02-04 15:47:01 +00:00
1236.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
1237.lean
1247.lean
1253.lean
1267.lean
1274.lean
1289.lean
1293.lean
1299.lean
1300.lean
1302.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
1305.lean
1308.lean
1311.lean
1333.lean
1337.lean
1342.lean
1359.lean
1360.lean
1361.lean
1361b.lean
1365.lean
1372.lean
1373.lean
1374.lean
1375.lean
1380.lean feat: improve simp trace formatting (#6951) 2025-02-04 15:47:01 +00:00
1385.lean
1389.lean
1408.lean
1411.lean
1419.lean
1420.lean
1426.lean
1435.lean
1436.lean
1441.lean
1547.lean
1549.lean
1558.lean
1575.lean
1615.lean
1650.lean
1674.lean
1679.lean
1684.lean
1686.lean
1692.lean
1697.lean feat: asynchronous kernel checking 2025-01-23 19:07:31 -07:00
1711.lean
1725.lean
1730.lean
1780.lean
1785.lean
1787.lean
1808.lean
1812.lean
1813.lean
1815.lean feat: improve simp trace formatting (#6951) 2025-02-04 15:47:01 +00:00
1822.lean
1829.lean
1841.lean
1842.lean
1848.lean
1850.lean
1851.lean
1852.lean
1869.lean
1882.lean
1883.lean
1886.lean
1892.lean
1900.lean
1901.lean feat: reorder tc subgoals according to out-params 2023-04-10 13:00:04 -07:00
1907.lean
1907orig.lean
1910.lean
1921.lean
1926.lean
1937.lean
1951.lean
1954.lean
1963.lean
1968.lean
1985.lean
1986.lean
2009.lean
2018.lean
2042.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
2044.lean
2058.lean
2073.lean
2074.lean
2079.lean
2095.lean
2136.lean
2137.lean
2143.lean
2159.lean feat: asynchronous kernel checking 2025-01-23 19:07:31 -07:00
2161.lean
2173.lean
2182.lean
2186.lean
2188.lean
2199.lean
2220.lean
2226.lean
2243.lean
2249.lean
2262.lean
2265.lean
2282.lean
2283.lean
2291.lean feat: asynchronous code generation (#6770) 2025-02-03 17:17:18 +00:00
2299.lean
2311.lean
2344.lean
2389.lean
2461.lean
2500.lean
2552.lean
2558.lean
2575.lean
2611.lean
2615.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
2649.lean
2669.lean
2670.lean
2672.lean
2689.lean
2690.lean
2710.lean
2736.lean
2810.lean
2835.lean
2843.lean
2846.lean chore: cleanup duplicate theorems (#7113) 2025-02-18 01:46:12 +00:00
2862.lean
2899.lean
2901.lean
2905.lean
2914.lean
2916.lean feat: asynchronous kernel checking 2025-01-23 19:07:31 -07:00
2939.lean
2942.lean
2961.lean test: more equational theorem generation tests (#6952) 2025-02-04 22:18:35 +00:00
2966.lean
3022.lean
3031.lean
3045.lean
3079.lean
3091.lean
3146.lean
3146.lean.expected.out
3150.lean feat: make structure parent projections nameable (#7100) 2025-02-18 07:38:13 +00:00
3214.lean
3219.lean test: more equational theorem generation tests (#6952) 2025-02-04 22:18:35 +00:00
3229.lean
3242.lean
3257.lean feat: improve simp trace formatting (#6951) 2025-02-04 15:47:01 +00:00
3313.lean feat: only direct parents of classes create projections (#5920) 2024-11-12 01:55:17 +00:00
3386.lean
3395.lean
3458_1.lean
3458_2.lean
3467.lean
3497.lean feat: language reference links and examples in docstrings (#7240) 2025-03-12 09:17:27 +00:00
3501.lean
3519.lean
3524.lean
3546.lean
3547.lean
3554.lean chore: additional newline before 'additional diagnostic information' message (#7169) 2025-02-23 23:27:33 +00:00
3643.lean
3686.lean
3705.lean
3706.lean
3710.lean
3713.lean
3731.lean
3740.lean
3745.lean
3807.lean feat: make structure parent projections nameable (#7100) 2025-02-18 07:38:13 +00:00
3922.lean fix: prevent exact? and apply? from suggesting invalid tactics (#7192) 2025-02-25 15:24:09 +00:00
3943.lean
3965.lean
3965_2.lean
3965_3.lean
3996.lean chore: additional newline before 'additional diagnostic information' message (#7169) 2025-02-23 23:27:33 +00:00
4051.lean
4064.lean
4086.lean
4101.lean
4144.lean
4171.lean feat: make structure parent projections nameable (#7100) 2025-02-18 07:38:13 +00:00
4203.lean chore: additional newline before 'additional diagnostic information' message (#7169) 2025-02-23 23:27:33 +00:00
4213.lean
4219.lean
4230.lean
4251.lean
4290.lean
4306.lean
4310.lean
4313.lean
4318.lean
4320.lean
4334.lean
4339.lean
4365.lean chore: additional newline before 'additional diagnostic information' message (#7169) 2025-02-23 23:27:33 +00:00
4381.lean
4390.lean
4398.lean
4405.lean
4406.lean
4413.lean
4462.lean
4465.lean
4534.lean
4547.lean
4555.lean
4561.lean
4573.lean
4585.lean
4595_slowdown.lean feat: make structure parent projections nameable (#7100) 2025-02-18 07:38:13 +00:00
4595_split.lean
4636.lean
4644.lean
4662.lean
4670.lean
4673.lean
4677.lean
4686.lean fix: make pretty printer escape identifiers that are tokens (#4979) 2024-09-07 21:28:44 +00:00
4751.lean
4761.lean
4768.lean
4773.lean
4851.lean
4861.lean
4888.lean
4920.lean
4928.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
4947.lean
4983.lean
4985.lean
5046.lean
5064.lean
5126.lean
5176.lean
5236.lean
5333.lean
5359.lean
5388.lean
5406.lean
5407.lean fix: prevent exact? and apply? from suggesting invalid tactics (#7192) 2025-02-25 15:24:09 +00:00
5417.lean
5424.lean
5455.lean
5475.lean
5565.lean
5634.lean
5660.lean
5664.lean
5667.lean feat: use realizeConst for all equation and unfold theorems (#7348) 2025-03-05 14:56:50 +00:00
5668.lean
5672.lean
5674.lean feat: present bv_decide counter examples for UIntX and enums better (#7033) 2025-02-11 11:01:40 +00:00
5689.lean
5755.lean
5818.lean
5993.lean
6043.lean
6065.lean fix: report replay kernel errors as standard diagnostics (#7471) 2025-03-13 18:45:46 +00:00
6067.lean
6086.lean
6090.lean
6117.lean
6123_cat_adjunction.lean feat: make structure parent projections nameable (#7100) 2025-02-18 07:38:13 +00:00
6123_mod_cast.lean
6164.lean feat: add simp? and dsimp? in conversion mode (#6593) 2025-01-10 01:42:17 +00:00
6199.lean
6263.lean
6354.lean
6467.lean
6694.lean fix: show error messages on name conflicts in mutual blocks (#6939) 2025-02-05 04:23:24 +00:00
6706.lean fix: move auxDeclToFullName to LocalContext to fix name (un)resolution (#7075) 2025-03-03 16:10:54 +00:00
6759.lean feat: allow anonymous equality proofs in match expressions (#6853) 2025-02-04 16:09:21 +00:00
6789.lean fix: consume mdata in casesOnStuckLHS when checking that major is fvar (#6791) 2025-01-29 14:32:11 +00:00
6927.lean fix: correctly collect let-rec fvars through delayed-assigned mvar (#7304) 2025-03-10 18:13:48 +00:00
6999.lean fix: ensure get_elem_tactic works in absence of goals (#7088) 2025-02-15 03:00:36 +00:00
7073.lean fix: move auxDeclToFullName to LocalContext to fix name (un)resolution (#7075) 2025-03-03 16:10:54 +00:00
7353.lean fix: abstractNestedProofs should see into the head of an application (#7353) 2025-03-06 20:08:38 +00:00
7405.lean fix: make the Subsingleton instance for Squash work for an arbitrary Sort (#7406) 2025-03-11 08:41:30 +00:00
7475.lean fix: bv_decide don't analyze terms under binders by accident (#7477) 2025-03-13 16:47:20 +00:00
abstractExpr.lean
ac_expr.lean
ac_rfl.lean
ack.lean feat: elaborate theorem bodies in parallel (#7084) 2025-03-14 07:50:42 +00:00
ACltBug.lean
adam1.lean
adamTC.lean
adamTC2.lean
add_suggestion.lean
addDecorationsWithoutPartial.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
addPPExplicitToExposeDiff.lean
aig_optimizations.lean
aig_shared.lean
aig_stress.lean
alex1.lean
alg.lean
alias.lean
allGoals.lean feat: elaborate theorem bodies in parallel (#7084) 2025-03-14 07:50:42 +00:00
and_intros.lean
andCasesOnBug.lean
anonymous_ctor_error_msg.lean
anonymousCtor.lean
appFinalizeIssue.lean
appIssue.lean
apply_tac.lean
applytransp.lean
approxDepth.lean
array1.lean fix: allow trailing comma in array syntax (#7055) 2025-02-16 19:26:23 +00:00
array_isEqvAux.lean feat: align List/Array/Vector.zip/zipWith/zipWithAll/unzip (#6840) 2025-01-29 07:58:17 +00:00
array_simp.lean
arrowDot.lean
arthur1.lean
arthur2.lean
as_aux_lemma.lean feat: builtin as_aux_lemma tactic and tree_tac simp attribute (#6823) 2025-02-03 08:34:29 +00:00
assertAfterBug.lean
aStructPerfIssue.lean
async_sleep.lean feat: implement basic async IO with timers (#6505) 2025-01-13 18:11:04 +00:00
async_surface_sleep.lean feat: implement basic async IO with timers (#6505) 2025-01-13 18:11:04 +00:00
atomValidation.lean
attachJp.lean
autoboundIssues.lean
autoLift.lean fix: make #check_failure's output be info (#6685) 2025-01-18 07:27:44 +00:00
autoLiftIssue.lean
autoparam.lean
auxinvariable.lean feat: omega to abstract its own proofs (#5998) 2025-03-10 12:39:30 +00:00
backtrackable_estate.lean
balg.lean
betaSimp.lean
bigctor.lean
bigmul.lean
bigop.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
bindCasesIssue.lean
binderNameHint.lean feat: binderNameHint (#6947) 2025-02-06 11:03:27 +00:00
binderNameHint_congr.lean feat: binderNameHint in congr (#7053) 2025-02-13 09:38:42 +00:00
binderNameHintScope.lean feat: binderNameHint (#6947) 2025-02-06 11:03:27 +00:00
binderNameHintSimp.lean feat: binderNameHint (#6947) 2025-02-06 11:03:27 +00:00
binderNotation.lean
binop.lean
binop_binrel_perf_issue.lean feat: make structure parent projections nameable (#7100) 2025-02-18 07:38:13 +00:00
binrec.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
binrel.lean
binrelmacros.lean
bitvec.lean
bitvec_fin_literal_norm.lean
bitvec_simproc.lean feat: make BitVec.getElem the simp normal form and use it in ext (#5498) 2025-02-16 00:04:56 +00:00
borrowBug.lean
bubble.lean
bugNatLitDiscrTree.lean
bv_arith.lean
bv_axiom_check.lean feat: add or/and/xor lemmas for BitVec/bv_normalize (#6872) 2025-01-31 13:27:43 +00:00
bv_bitblast_stress.lean
bv_bitwise.lean
bv_cast.lean
bv_counterexample.lean refactor: the AIG framework to track negations in a more efficient way (#7381) 2025-03-17 17:33:49 +00:00
bv_decide_bool.lean perf: improve bv_decide preprocessing based on Bitwuzla optimisations (#6641) 2025-01-15 12:09:43 +00:00
bv_decide_nat.lean
bv_decide_rewriter.lean feat: bv_normalize pass: AC normalization of multiplication (#7461) 2025-03-18 08:28:35 +00:00
bv_decide_rewriter_ac_nf.lean feat: bv_normalize pass: AC normalization of multiplication (#7461) 2025-03-18 08:28:35 +00:00
bv_enums.lean feat: bv_decide support enum inductive matches with default branches (#7417) 2025-03-10 14:05:04 +00:00
bv_errors.lean
bv_extract.lean
bv_inequality.lean
bv_llvm.lean
bv_math_lit_perf.lean
bv_popcount.lean
bv_preprocess_stress.lean
bv_reflection_stress.lean
bv_relation.lean feat: bv_decide remove casts (#7390) 2025-03-07 22:40:53 +00:00
bv_shift.lean
bv_sint.lean feat: add IntX and ISize support for bv_decide (#7269) 2025-02-28 10:33:11 +00:00
bv_structures.lean feat: add IntX and ISize support for bv_decide (#7269) 2025-02-28 10:33:11 +00:00
bv_substructure.lean
bv_uint.lean feat: add IntX and ISize support for bv_decide (#7269) 2025-02-28 10:33:11 +00:00
bv_uninterpreted.lean
bv_unused.lean feat: present bv_decide counter examples for UIntX and enums better (#7033) 2025-02-11 11:01:40 +00:00
bv_will_overflow.lean
by_cases.lean chore: additional newline before 'additional diagnostic information' message (#7169) 2025-02-23 23:27:33 +00:00
byAsSorry.lean
byteSliceIssue.lean
calc.lean
calcBug.lean
calcInType.lean
canonM_exists_fun.lean
casePrime.lean
casesAnyTypeIssue.lean
casesRec.lean
casesTactic.lean
casesUsing.lean feat: induction tactic to err on extra targets (#7224) 2025-02-25 20:53:16 +00:00
caseTacInMacros.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
catchThe.lean
cceScoping.lean fix: properly handle scoping of join point candidates in cce (#7398) 2025-03-08 18:10:41 +00:00
cdotAtSimpArg.lean
cdotTests.lean
change.lean
check.lean
check_failure.lean
checkAssignmentIssue.lean
choiceExpectedTypeBug.lean
choiceMacroRules.lean
class_inductive.lean
classAbbrev.lean
classical.lean
cleanup_forallTelescope.lean feat: add cleanupAnnotations parameter to forallTelescope methods (#4180) 2024-05-15 22:19:07 +00:00
closure1.lean
codeBindUnreachIssue.lean
coeAttrs.lean
coeIssue1.lean
coeIssue2.lean
coeIssue3.lean
coeIssues4.lean
coelambda.lean
CoeNew.lean
coeOutParamIssue.lean
coeOutParamIssue2.lean
coeSort1.lean
coeSort2.lean
combinatorsAndWF.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
CommandExtOverlap.lean
compatibleTypesBugAtLCNF.lean
compatibleTypesEtaIssue.lean
compiler_erase_bug.lean
compiler_proj_bug.lean feat: asynchronous kernel checking 2025-01-23 19:07:31 -07:00
CompilerCSE.lean
CompilerFindJoinPoints.lean
CompilerFloatLetIn.lean
CompilerProbe.lean
CompilerPullInstances.lean
CompilerSimp.lean
compilerTest1.lean
computedFields.lean
concatElim.lean
congrReserved.lean chore: complete variable name linting for Vector (#7154) 2025-02-20 02:42:50 +00:00
congrTactic.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
congrThm.lean
congrThm2.lean
constantCompilerBug.lean
constFun.lean
constFun2.lean
constProp.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
constructor_as_variable.lean
contra.lean
contradiction1.lean
contradictionExfalso.lean
contradictionLoop.lean
conv1.lean
conv2.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
conv_arg.lean
convcalc.lean
core.lean
crashDiv0.lean
crlfToLf.lean
csimp_type_error.lean
csimpAttrFn.lean
ctorAutoParams.lean
currentDir.lean
customEliminators.lean
Daniel1.lean
deBruijn.lean
decAuxBug.lean
decClassical.lean
decEq.lean
decidability_timeout.lean
Decidable-decide-erasure.lean
decidelet.lean
decideNative.lean
decideTactic.lean
decideTacticKernel.lean feat: elaborate theorem bodies in parallel (#7084) 2025-03-14 07:50:42 +00:00
declareConfigElabBug.lean
declareConfigElabIssue.lean
decreasingTacticUpdatedEnvIssue.lean
deep1.lean
def1.lean
def2.lean
def3.lean
def4.lean
def5.lean
def6.lean
def7.lean
def8.lean
def9.lean
def10.lean
def11.lean
def12.lean
def13.lean
def14.lean
def15.lean
def16.lean
def17.lean
def18.lean
def19.lean
def20.lean
defaultEliminator.lean
defaultInstBacktrackIssue.lean
defaulValueParamIssue.lean
DefEqAssignBug.lean feat: better #eval command (#5627) 2024-10-08 20:51:46 +00:00
defEqVsWhnfI.lean
delabApp.lean
delabMatch.lean
delabName.lean
delabProjectionApp.lean
delabStructInst.lean
depElim1.lean
depFieldIssue.lean
depHd.lean
deq.lean
deriv.lean
derivingBEq.lean
derivingHashable.lean
derivingInhabited.lean
derivingNonempty.lean
derivingRepr.lean chore: deprecate List.iota (#6708) 2025-01-21 02:32:35 +00:00
derivingToExpr.lean
diagnostics.lean fix: add workaround for MessageData limitations (#6669) 2025-01-16 16:58:20 +00:00
diagnosticsMsgOptional.lean chore: additional newline before 'additional diagnostic information' message (#7169) 2025-02-23 23:27:33 +00:00
diagRec.lean fix: add workaround for MessageData limitations (#6669) 2025-01-16 16:58:20 +00:00
diamond1.lean
diamond2.lean
diamond3.lean
diamond4.lean
diamond5.lean
diff.lean
discrRefinement.lean
discrRefinement2.lean
discrRefinement3.lean
discrTreeKey.lean fix: #discr_tree_simp_key shouldn't look into lhs of ≠ (#6936) 2025-02-04 08:43:12 +00:00
discrTreeOffset.lean
discrTreeSimp.lean
do_eqv.lean
do_eqv_proofs.lean
docstringRewrites.lean feat: language reference links and examples in docstrings (#7240) 2025-03-12 09:17:27 +00:00
doElemAsTermNotation.lean
dofun_prec.lean
doLetElse.lean
dollarProjIssue.lean
doNotation1.lean
doNotation2.lean
doNotation3.lean
doNotation4.lean
doNotation5.lean
doNotation6.lean
Dorais1.lean
dotNameIssue.lean
dotNotationAndDefaultInstance.lean
dotNotationRecDecl.lean
doTrailingAtEOI.lean
dottedCtorNamedArgPattern.lean
dottedNameBug.lean
dsimp1.lean
dsimp2.lean
dsimp_bv_simproc.lean feat: asynchronous kernel checking 2025-01-23 19:07:31 -07:00
dsimpNatLitIssue.lean
dsimproc.lean
dvd_simproc.lean feat: simprocs for Int and Nat divides predicates (#7078) 2025-02-14 05:43:38 +00:00
DVec.lean
dynamic.lean
eagerInliningIssue.lean
elab_cmd.lean
elabAsElim.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
elabCmd.lean
elabIte.lean
eliminatorImplicitTargets.lean
elimOptParam.lean
elseCaseArrow.lean
elseIfConfusion.lean
emptycOverloadIssues.lean
emptyLcnf.lean fix: don't create reduced arity LCNF decls with no params (#7086) 2025-02-27 01:23:34 +00:00
enumDecEq.lean
enumNoConfusionIssue.lean
eq_some_iff_get_eq_issue.lean
eqndrecEtaLCNFIssue.lean
eqnOptions.lean
eqnsAtSimp.lean
eqnsAtSimp2.lean
eqnsAtSimp3.lean
eqnsPrio.lean
eqnsProjections.lean
eqnsReducible.lean feat: elaborate theorem bodies in parallel (#7084) 2025-03-14 07:50:42 +00:00
eqTheoremForVec.lean
eqThm.lean
eqThmWithMoreThanOneAsPattern.lean
eqValue.lean
erased.lean fix: don't create reduced arity LCNF decls with no params (#7086) 2025-02-27 01:23:34 +00:00
eraseReps.lean
eraseSuffix.lean
erasureConfusion.lean
etaFirst.lean
etaStruct.lean
etaStructProofIrrelIssue.lean
eval.lean
eval_unboxed_const.lean
evalBuiltinInit.lean
evalconst.lean
evalDo.lean
evalInit.lean
evalProp.lean
evalTacticBug.lean
exfalsoBug.lean
exists.lean
exp.lean
expandAbbrevAtIsClass.lean
expandWhereStructInstIssue.lean
expectedTypePropagation.lean
explicitApp.lean
explicitMotive.lean
explictOpenDeclIssue.lean
exposeNames.lean feat: expose_names tactic (#6935) 2025-02-04 00:53:31 +00:00
expr1.lean
expr_maps.lean
ExprLens.lean
ext.lean feat: asynchronous kernel checking 2025-01-23 19:07:31 -07:00
ext1.lean
extensibleTacticBug.lean
extern.lean
extmacro.lean
false_or_by_contra.lean
falseElimAtSimpLocalDecl.lean
fib_correct.lean chore: fib_correct monadic reasoning example as a test (#6647) 2025-01-15 01:58:15 +00:00
fieldAbbrevInPat.lean
fieldAutoBound.lean
fieldDefaultValueWithoutType.lean
fieldIssue.lean
fieldNamesWithMinus.lean
fieldTypeBug.lean
filter.lean chore: deprecate List.iota (#6708) 2025-01-21 02:32:35 +00:00
fin_two_pow.lean
finally.lean
finDotCtor.lean
finLit.lean
finMatch.lean
fixedParams.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
fixedParamsAnnot.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
fixedParamsDep.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
fixedParamsReorder.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
fixedParamsStructDeps.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
flat_expr.lean
float1.lean
float32.lean fix: Float32.ofInt (#7277) 2025-03-02 23:22:35 +00:00
float_cases_bug.lean
float_conversions.lean feat: conversions between Float and finite integers (#7083) 2025-02-17 15:42:10 +00:00
float_from_bignum.lean
floatarray.lean
floatBits.lean
floatOptParam.lean
foApprox.lean
foldConsts.lean
foldLits.lean
foldProjs.lean
forBodyResultTypeIssue.lean
forIn_phashset.lean feat: add ForIn instance for PHashSet (#7214) 2025-02-24 20:37:45 +00:00
forInColErr.lean refactor: elaborate forIn notation without extra let (#6977) 2025-02-08 10:32:34 +00:00
forInElabBug.lean
forInPArray.lean chore: deprecate List.iota (#6708) 2025-01-21 02:32:35 +00:00
forInRangeWF.lean
forInReturnPropagation.lean
forInUniv.lean
formatterTokenTable.lean
forOutParamIssue.lean
forParallel.lean
french_quote.lean
frontend_meeting_2022_09_13.lean
fun.lean
fun_cases.lean feat: functional cases theorem for non-recursive functions (#6261) 2025-01-21 10:16:42 +00:00
funext.lean
funind_demo.lean
funind_expr.lean
funind_fewer_levels.lean
funind_mutual_dep.lean
funind_proof.lean
funind_structural.lean feat: revision of Nat/Int lemmas (#7435) 2025-03-12 05:52:09 +00:00
funind_structural_mutual.lean
funind_tests.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
funInduction.lean feat: fun_induction foo (no arguments) (#7101) 2025-02-18 12:27:21 +00:00
funinduction_generalize.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
funinduction_ident.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
funMatchIssue.lean
fvarSubset.lean
generalize.lean
generalizeMany.lean feat: asynchronous kernel checking 2025-01-23 19:07:31 -07:00
generalizeTelescope.lean feat: cleanup of get and back functions on List/Array (#7059) 2025-02-17 01:43:45 +00:00
genindices.lean
getline_crash.lean
grind_assoc.lean feat: more grind tests (#6650) 2025-01-15 23:00:23 +00:00
grind_attrs.lean feat: elaborate theorem bodies in parallel (#7084) 2025-03-14 07:50:42 +00:00
grind_beta.lean feat: beta reduction in grind (#6700) 2025-01-19 21:29:24 +00:00
grind_bigstep.lean feat: better support for inductive predicates in grind (#6854) 2025-01-29 18:17:34 +00:00
grind_bool_prop.lean feat: normalize != and == in grind (#6870) 2025-01-30 16:00:18 +00:00
grind_canon_bug.lean fix: grind canonicalizer (#6585) 2025-01-09 02:23:46 +00:00
grind_canon_insts.lean fix: grind push new fact (#7532) 2025-03-17 19:14:08 +00:00
grind_canon_types.lean feat: beta reduction in grind (#6700) 2025-01-19 21:29:24 +00:00
grind_cases.lean feat: case splitting in grind (#6717) 2025-01-20 22:44:56 +00:00
grind_cases_tac.lean
grind_cat.lean chore: cleanup grind tests (#6871) 2025-01-30 17:51:45 +00:00
grind_cat2.lean chore: cleanup grind tests (#6871) 2025-01-30 17:51:45 +00:00
grind_congr.lean feat: beta reduction in grind (#6700) 2025-01-19 21:29:24 +00:00
grind_congr1.lean
grind_constProp.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
grind_ctor_ematch.lean feat: simp diagnostics in grind (#6902) 2025-02-23 17:55:17 +00:00
grind_cutsat_auto.lean feat: add [grind cases eager] Subtype (#7540) 2025-03-18 01:19:22 +00:00
grind_cutsat_cooper.lean feat: tight inequalities using divisibility constraints in cutsat (#7401) 2025-03-09 00:23:32 +00:00
grind_cutsat_decompose.lean fix: cutsat conflict resolution bug (#7403) 2025-03-09 03:58:30 +00:00
grind_cutsat_diseq_1.lean feat: disequalities in cutsat (#7244) 2025-02-26 17:26:59 +00:00
grind_cutsat_diseq_2.lean doc: cutsat procedure (#7262) 2025-02-27 21:15:34 +00:00
grind_cutsat_diseq_3.lean feat: non-chronological backtracking for cutsat (#7284) 2025-03-01 23:19:11 +00:00
grind_cutsat_diseq_cooper.lean feat: cutsat missing case: disequality+inequality+divisibility conflict (#7373) 2025-03-07 01:36:29 +00:00
grind_cutsat_div_1.lean feat: not divides in cutsat (#7536) 2025-03-17 22:29:42 +00:00
grind_cutsat_div_mod.lean fix: grind push new fact (#7532) 2025-03-17 19:14:08 +00:00
grind_cutsat_eq_1.lean doc: cutsat procedure (#7262) 2025-02-27 21:15:34 +00:00
grind_cutsat_le_1.lean feat: cutsat counterexamples (#7278) 2025-02-28 19:05:27 +00:00
grind_cutsat_le_2.lean test: cutsat cooper resolution (#7354) 2025-03-06 00:40:38 +00:00
grind_cutsat_nat_dvd.lean fix: missing reset at decision stack in cutsat (#7538) 2025-03-18 00:21:56 +00:00
grind_cutsat_nat_eq.lean feat: Int.toNat and Int.natAbst in cutsat (#7537) 2025-03-17 23:29:21 +00:00
grind_cutsat_nat_le.lean feat: Nat equalities and disequalities in cutsat (#7501) 2025-03-15 21:24:04 +00:00
grind_cutsat_tests.lean feat: missing normalization rules for div and mod in grind (#7514) 2025-03-16 23:00:12 +00:00
grind_cutsat_upper_bug.lean fix: bug in cutsat model construction (#7396) 2025-03-08 15:58:20 +00:00
grind_dep_match_overlap.lean fix: offset constraint propagation in grind (#6801) 2025-01-27 23:43:31 +00:00
grind_diseq.lean
grind_diseq_api.lean feat: add Grind.mkDiseqProof? (#7231) 2025-02-25 23:40:07 +00:00
grind_ematch1.lean chore: cleanup of remaining Array-specific material (#7253) 2025-02-27 10:51:30 +00:00
grind_ematch2.lean feat: infrastructure for supporting Nat in cutsat (#7394) 2025-03-08 08:36:58 +00:00
grind_ematch_patterns.lean chore: improve grind pattern pretty printer (#6910) 2025-02-03 03:04:33 +00:00
grind_eq.lean feat: Nat equalities and disequalities in cutsat (#7501) 2025-03-15 21:24:04 +00:00
grind_eq_bwd.lean feat: attributes [grind =>] and [grind <=] (#6897) 2025-02-01 04:41:19 +00:00
grind_eq_pattern.lean chore: improve grind pattern pretty printer (#6910) 2025-02-03 03:04:33 +00:00
grind_erase_attr.lean feat: improve pattern selection heuristic in grind (#6880) 2025-01-31 02:16:15 +00:00
grind_eval_suggest.lean feat: exact? in try? (#6995) 2025-02-07 22:43:30 +00:00
grind_exfalso.lean feat: exfalso in grind (#7510) 2025-03-16 17:25:19 +00:00
grind_guide.lean chore: cleanup of remaining Array-specific material (#7253) 2025-02-27 10:51:30 +00:00
grind_heq_proof_issue.lean
grind_implies.lean feat: add support for splitting on <-> to grind (#6607) 2025-01-12 02:25:02 +00:00
grind_ite_split_issue.lean fix: if-then-else split + normalization issue in grind (#7392) 2025-03-07 23:05:59 +00:00
grind_lazy_ite.lean feat: Nat equalities and disequalities in cutsat (#7501) 2025-03-15 21:24:04 +00:00
grind_list.lean chore: cleanup grind tests (#6871) 2025-01-30 17:51:45 +00:00
grind_many_eqs.lean feat: beta reduction in grind (#6700) 2025-01-19 21:29:24 +00:00
grind_mark_nested_proofs_bug.lean fix: markNestedProofs (#7355) 2025-03-06 00:51:13 +00:00
grind_match1.lean feat: hide grind auxiliary gadgets in messages (#6882) 2025-01-31 05:10:59 +00:00
grind_match2.lean chore: cleanup grind tests (#6871) 2025-01-30 17:51:45 +00:00
grind_match_cond_contra.lean feat: close goals using match-expression conditions in grind (#6783) 2025-01-26 17:13:11 +00:00
grind_match_eq_propagation.lean fix: grind using reducible transparency setting (#7102) 2025-02-16 22:30:04 +00:00
grind_natCast.lean feat: infrastructure for supporting Nat in cutsat (#7394) 2025-03-08 08:36:58 +00:00
grind_nested_proof_issue.lean
grind_nested_proofs.lean feat: hide grind auxiliary gadgets in messages (#6882) 2025-01-31 05:10:59 +00:00
grind_norm_levels.lean feat: beta reduction in grind (#6700) 2025-01-19 21:29:24 +00:00
grind_offset.lean feat: Nat equalities and disequalities in cutsat (#7501) 2025-03-15 21:24:04 +00:00
grind_offset_cnstr.lean chore: cleanup and missing grind normalization rules (#7095) 2025-02-15 23:45:35 +00:00
grind_offset_model.lean feat: infrastructure for supporting Nat in cutsat (#7394) 2025-03-08 08:36:58 +00:00
grind_palindromes.lean feat: missing propagation rules in grind (#6858) 2025-01-29 23:40:33 +00:00
grind_params.lean feat: simp diagnostics in grind (#6902) 2025-02-23 17:55:17 +00:00
grind_pattern1.lean chore: linting variable names in List/Array (#7146) 2025-02-19 12:45:02 +00:00
grind_pattern2.lean chore: improve grind pattern pretty printer (#6910) 2025-02-03 03:04:33 +00:00
grind_pattern_proj.lean chore: post-#7100 cleanup (#7196) 2025-02-23 22:46:22 +00:00
grind_Poly_mul_0_bug.lean fix: Poly.mul p 0 (#7397) 2025-03-08 16:57:13 +00:00
grind_pre.lean feat: infrastructure for supporting Nat in cutsat (#7394) 2025-03-08 08:36:58 +00:00
grind_prop_arrow.lean
grind_propagate_connectives.lean chore: cleaunp grind tests (#6616) 2025-01-13 00:07:48 +00:00
grind_regression.lean feat: Nat equalities and disequalities in cutsat (#7501) 2025-03-15 21:24:04 +00:00
grind_shelf.lean
grind_split.lean feat: case splitting in grind (#6717) 2025-01-20 22:44:56 +00:00
grind_split_data.lean fix: case split on data in grind (#6781) 2025-01-26 02:14:08 +00:00
grind_split_issue.lean feat: simp diagnostics in grind (#6902) 2025-02-23 17:55:17 +00:00
grind_t1.lean feat: Nat equalities and disequalities in cutsat (#7501) 2025-03-15 21:24:04 +00:00
grind_trace.lean feat: attributes [grind =>] and [grind <=] (#6897) 2025-02-01 04:41:19 +00:00
grind_try_exact.lean feat: exact? in try? (#6995) 2025-02-07 22:43:30 +00:00
grind_try_trace.lean fix: missing indents in Try this message (#7191) 2025-02-25 16:55:50 +00:00
grind_usr.lean feat: improve pattern selection heuristic in grind (#6880) 2025-01-31 02:16:15 +00:00
guard_expr.lean
guard_msgs.lean chore: additional newline before 'additional diagnostic information' message (#7169) 2025-02-23 23:27:33 +00:00
guardexpr.lean
handleLocking.lean
hashableBug.lean
hashmap-implicits.lean chore: rename HashMap.empty to HashMap.emptyWithCapacity (#7447) 2025-03-12 23:01:18 +00:00
hashmap-toList-simps.lean feat: verify toList for hash maps (#6954) 2025-02-18 13:10:03 +00:00
hashmap.lean
haveDestruct.lean
haveI.lean
haveTactic.lean
hcongr.lean
heapSort.lean
heqSubst.lean
hlistOverload.lean
hmul2.lean
hmulDefaultIntance.lean
ifcongr.lean
iffRefl.lean
ifThenElseIssue.lean
ifThenElseIssue2.lean
impByNameResolution.lean
impLambdaTac.lean
implicitApplyIssue.lean
implicitLambdaLocalWithoutType.lean
implicitRflProofs.lean
implicitTypesRecCoe.lean
inaccessibleAnnotDefEqIssue.lean
incmd.lean
ind_cmd_bug.lean
ind_whnf.lean
ind_whnf2.lean
index_variables_linter.lean chore: fix variable names in List lemmas (#6953) 2025-02-05 09:49:14 +00:00
induction1.lean feat: add generalization hypotheses to induction tactic (#7103) 2025-02-18 03:46:23 +00:00
inductionAltExplicit.lean
inductionCheckAltNames.lean
inductionLetIssue.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
inductionParse.lean
inductionTacticBug.lean
inductive1.lean
inductive2.lean feat: ignore {} annotation at constructors 2022-04-13 08:30:21 -07:00
inductive_mutual.lean
inductive_pred.lean
inductive_rec_proj.lean
inductive_typestar.lean
inductive_univ.lean feat: make structure parent projections nameable (#7100) 2025-02-18 07:38:13 +00:00
inductiveIndicesIssue.lean
indUsingLet.lean
inferForallTypeLCNF.lean
infixprio.lean
info_trees.lean feat: elaborate theorem bodies in parallel (#7084) 2025-03-14 07:50:42 +00:00
inj1.lean
inj2.lean
injectionBug.lean
injections1.lean
injectionsIssue.lean
injective.lean
injHEq.lean
injIssue.lean
injSimp.lean
inline_fn.lean
inlineIfReduceLCNF.lean
inlineLCNFIssue.lean
inlineLoop.lean
inlineProjInstIssue.lean
inliner_loop.lean feat: asynchronous kernel checking 2025-01-23 19:07:31 -07:00
inlineWithNestedRecIssue.lean
instanceIssues.lean
instances.lean
instanceWhere.lean
instanceWhereDecls.lean
instEtaIssue.lean
instPatVar.lean
instprio.lean
instuniv.lean
int_complement_shiftRight.lean
int_to_nat_bug.lean
int_toBitVec.lean feat: tag lemmas 2025-01-15 15:17:36 +01:00
internalizeCasesIssue.lean
interp.lean
interp2.lean
introLetFun.lean
intromacro.lean chore: use #guard_msgs in run tests (#4175) 2024-05-16 00:38:31 +00:00
IO_test.lean chore: deprecate List.iota (#6708) 2025-01-21 02:32:35 +00:00
ioRandomBytes.lean
irCompilerBug.lean
irreducibleIssue.lean
isDefEqCheckAssignmentBug.lean
isDefEqConstApproxIssue.lean
isDefEqIssue.lean
isDefEqMVarSelfIssue.lean
isDefEqPerfIssue.lean
isDefEqProjIssue.lean chore: additional newline before 'additional diagnostic information' message (#7169) 2025-02-23 23:27:33 +00:00
isDefEqProjPerfIssue.lean
issue2102.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
issue2108.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
issue2113.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
issue2628.lean
issue2883.lean
issue2925.lean
issue2975.lean
issue2982.lean
issue3175.lean
issue3204.lean
issue3212.lean
issue3770.lean
issue3848.lean
issue4063.lean
issue4146.lean fix: FunInd to clear match discriminants if possible 2025-02-17 18:21:10 +01:00
issue4394.lean
issue4540.lean fix: recursion over predicates: add some whnf sprinkles (#5136) 2024-08-29 16:55:54 +00:00
issue4650.lean
issue4671.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
issue4684.lean
issue4726.lean
issue5027.lean
issue5061.lean
issue5347.lean
issue5384.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
issue5562.lean
issue5602.lean
issue5630.lean
issue5661.lean
issue5699.lean
issue5726.lean
issue5767.lean
issue5828.lean
issue5836.lean
issue5903.lean
issue6015.lean
issue6281.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
issue6531.lean fix: strip optional parameters when elaborating the termination hints (#7335) 2025-03-05 18:15:49 +00:00
issue6786.lean fix: more robust equational theorems generation for partial_fixpoint (#6790) 2025-01-27 14:00:55 +00:00
issue7318.lean fix: allow simp dischargers to add aux decls to the environment (#7362) 2025-03-06 16:00:59 +00:00
issue7322.lean chore: unconditionally re-enable realizeConst (#7334) 2025-03-11 16:39:17 +00:00
issue7332.lean fix: allow aux decls to be generated by decreasing_by tactics (#7333) 2025-03-04 18:42:36 +00:00
issue7408.lean fix: WellFounded preprocessing: use dsimp (#7409) 2025-03-09 22:19:16 +00:00
ite_dsimproc.lean
james1.lean
jason1.lean
json.lean
json_empty.lean
kernel1.lean
kernel2.lean
kernel_maxheartbeats.lean
kernelInterrupt.lean
kevin.lean
krivine.lean
kronRWIssue.lean
KyleAlg.lean
KyleAlgAbbrev.lean
lazyListRotateUnfoldProof.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
lazylistThunk.lean
lazyUnfoldingPerfIssue.lean
lcnf1.lean
lcnf2.lean
lcnf3.lean
lcnf4.lean
lcnf_simp_let.lean
lcnfBinderNameBug.lean
lcnfCastIssue.lean
lcnfCheckIssue.lean
lcnfErasure.lean feat: add proper erasure of type dependencies in LCNF (#6678) 2025-01-21 02:07:16 +00:00
lcnfEtaExpandBug.lean
lcnfInferProjTypeBug.lean
lcnfInferProjTypeIssue.lean
lcnfInliningIssue.lean
lcnfIssue.lean
lean3_zulip_issues_1.lean
lean_nat_bitwise.lean
lean_nat_gcd.lean
left_right.lean
lemma.lean
let_Issue.lean
letBRecOnIssue.lean
letDeclSimp.lean
letFunUnusedVarBug.lean
letMVar.lean
letrecInProofs.lean
letrecInThm.lean
letrecWFIssue.lean
level.lean
levelNamesInTacticMode.lean
levelNGen.lean
lex.lean
liaByRefl.lean refactor: cutsat (#7186) 2025-02-22 17:25:42 +00:00
libuv.lean
liftMethodInMacrosIssue.lean
LiftMethodIssue.lean
linearByRefl.lean chore: remove dead code from Nat/Linear.lean (#7042) 2025-02-12 02:14:00 +00:00
linearCategory_perf_issue.lean feat: make structure parent projections nameable (#7100) 2025-02-18 07:38:13 +00:00
list_monadic_functions.lean feat: missing monadic functions on List/Array/Vector (#6845) 2025-01-29 12:19:30 +00:00
list_simp.lean feat: mark forIn_pure_yield lemmas simp (#7433) 2025-03-14 00:28:23 +00:00
list_variables_linter.lean chore: linting variable names in List/Array (#7146) 2025-02-19 12:45:02 +00:00
listDecEq.lean
listtostring.lean
litToCtor.lean
localNameResolutionWithProj.lean
localParsers.lean
lrat_roundtrip.lean
macro.lean
macro2.lean
macro3.lean
macro_macro.lean
macroid.lean
macroParams.lean
manyAritySyntax.lean
mapTR.lean
match1.lean
match_eqns_bug.lean fix: match equality generation (#6719) 2025-01-21 02:05:37 +00:00
match_expr.lean
match_expr_expected_type_issue.lean
match_expr_meta_modifier.lean
match_expr_perf.lean
match_int_lit_issue.lean
match_lit_fin_cover.lean
match_lit_issues.lean
match_lit_regression.lean
match_unit.lean
matchArrayLit.lean
matchDiscrType.lean
matchEqnsHEqIssue.lean
matchEqs.lean
matchEqsBug.lean fix: realizeConst fixes (#7272) 2025-02-28 14:59:13 +00:00
matcherElimUniv.lean
matchGenBug.lean
matchGenIssue.lean
matchNoPostponing.lean
matchRw.lean
matchtac.lean
matchUnifyBug.lean
matchVarIssue.lean
matchWithSearch.lean
mathlibetaissue.lean feat: make structure parent projections nameable (#7100) 2025-02-18 07:38:13 +00:00
mathport18.lean
mathport_issue16.lean
matrix.lean
may_postpone_tc.lean
maze.lean
mergeSort.lean chore: additional newline before 'additional diagnostic information' message (#7169) 2025-02-23 23:27:33 +00:00
mergeSortCPDT.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
messageKind.lean
meta.lean
meta1.lean
meta2.lean
meta3.lean
meta4.lean
meta5.lean
meta6.lean
meta7.lean
methodsRetInhabited.lean
Miller1.lean
missingDeclName.lean
missingExplicitWithForwardNamedDep.lean
missingSizeOfArrayGetThm.lean
mixedMacroRules.lean
mixfix.lean
mjissue.lean
modAsClasses.lean
monadCache.lean
monadControl.lean
MonadControl_tutorial.lean
monotone.lean
mul_match_pattern.lean chore: mark Mul.mul and HMul.hMul as match_pattern (#6863) 2025-01-31 05:39:33 +00:00
mulcomm.lean
multiTargetCasesInductionIssue.lean
mut_ind_wf.lean
mutualDefThms.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
mutualWithCompositeNames.lean
mutwf1.lean
mutwf2.lean
mutwf3.lean
mutwf4.lean
namePatEqThm.lean
namespaceHyg.lean
namespaceIssue.lean
namespaceResolution.lean
nary_nomatch.lean
nat_mod_defeq.lean
nativeReflBackdoor.lean
natlit.lean
nested_inductive.lean
nested_match_bug.lean
nestedDo.lean
nestedInductiveConstructions.lean
nestedInductiveIssue.lean
nestedInductiveRecType.lean
nestedIssueMatch.lean
nestedrec.lean
nestedtc.lean
nestedTypeFormers.lean
nestedWF.lean
net_addr.lean feat: Std.Net.Addr (#6563) 2025-01-09 09:33:03 +00:00
new_compiler.lean
new_frontend2.lean
new_inductive.lean
new_inductive2.lean
newfrontend1.lean
newfrontend2.lean
newfrontend3.lean
newfrontend5.lean
nicerNestedDos.lean
no_grind_constProp.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
no_simproc_usize.lean
nofun1.lean
noindexAnnotation.lean
nomatch_regression.lean
nomatch_tac.lean
noncomp.lean
noncomputable_bug.lean
nonrec.lean
norm_cast.lean
numChars.lean
obtain.lean
offsetIssue.lean
ofNat_class.lean
ofNatNormNum.lean
omega.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
omega_examples.lean
omegaCanon.lean
omegaDischarger.lean
opaqueNewCodeGen.lean
openInScopeBug.lean
openTermTactic.lean feat: open in terms and tatics 2021-03-06 15:33:00 -08:00
optParam.lean
Ord.lean chore: fixing short-circuiting issue in Ordering.then (#6907) 2025-02-03 00:44:45 +00:00
overAndPartialAppsAtWF.lean
overloaded.lean
overloadsAndDelayedCoercions.lean
panicAtCheckAssignment.lean
parray1.lean chore: deprecate List.iota (#6708) 2025-01-21 02:32:35 +00:00
parsePrelude.lean
parserAliasShadow.lean
parserQuot.lean
partial1.lean
partial_fixpoint.lean fix: suggest correct trace option name in partial_fixpoint error message (#6774) 2025-01-25 14:42:15 +00:00
partial_fixpoint_aeneas.lean feat: partial_fixpoint: partial functions with equations (#6355) 2025-01-21 09:54:30 +00:00
partial_fixpoint_aeneas2.lean feat: partial_fixpoint: partial functions with equations (#6355) 2025-01-21 09:54:30 +00:00
partial_fixpoint_coinductive_pred.lean feat: partial_fixpoint: partial functions with equations (#6355) 2025-01-21 09:54:30 +00:00
partial_fixpoint_explicit.lean feat: partial_fixpoint: partial functions with equations (#6355) 2025-01-21 09:54:30 +00:00
partial_fixpoint_f91.lean test: expand f91 test (#7421) 2025-03-10 17:15:54 +00:00
partial_fixpoint_induct.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
partial_fixpoint_monotonicity.lean feat: partial_fixpoint: partial functions with equations (#6355) 2025-01-21 09:54:30 +00:00
partial_fixpoint_mutual.lean feat: partial_fixpoint: partial functions with equations (#6355) 2025-01-21 09:54:30 +00:00
partial_fixpoint_probability.lean feat: partial_fixpoint: partial functions with equations (#6355) 2025-01-21 09:54:30 +00:00
partial_fixpoint_split.lean feat: partial_fixpoint: partial functions with equations (#6355) 2025-01-21 09:54:30 +00:00
partialApp.lean
partialDelta.lean
patbug.lean
pendingInstBug.lean
pendingMVarIssue.lean
postponeBinRelIssue.lean
posView.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
ppMaxSteps.lean
ppMVars.lean
ppParens.lean
PProd_syntax.lean
PPTopDownAnalyze.lean
ppUsingAnonymousConstructor.lean
precDSL.lean
prefixTableStep.lean refactor: simpMatch to not etaStruct (#6901) 2025-02-01 19:04:05 +00:00
prelude-injectivity.lean feat: try? tactic (#6905) 2025-02-02 06:37:49 +00:00
premise_selection.lean feat: premise selection API (#7061) 2025-02-14 04:08:18 +00:00
primProjEtaIssue.lean
print_cmd.lean
printDecls.lean
printEqns.lean
prioDSL.lean
privateCtor.lean
processGenDiseqBug.lean
proj_delta_issue.lean
projDefEq2.lean
proofAsSorry.lean
proofDataConfusionBug.lean
proofIrrelFVar.lean
propagateExpectedType.lean
prv.lean
psumAtWF.lean
ptrAddr.lean
qualifiedNamesRec.lean
quasi_pattern_unification_approx_issue.lean
quotInd.lean
range.lean
Rat.lean fix: Rat.floor and Rat.ceil (#7294) 2025-03-02 22:50:36 +00:00
rational.lean
rawStrings.lean
rc_tests.lean
rcases.lean
rcases1.lean
readerThe.lean
recCommonPrefixAlpha.lean
recInfo1.lean
recommendedSpelling.lean chore: fix typo in test (#7460) 2025-03-12 16:43:35 +00:00
reduce1.lean
reduce2.lean
reduce3.lean
reducibilityAttrValidation.lean
reductionBug.lean
refl.lean
reflectiveIndPred.lean
regressions3210.lean
Reid1.lean
renameI.lean
renaming.lean
Reparen.lean
repeat.lean
repeatConv.lean
replace.lean
replace_tac.lean
repr_empty.lean
reserved.lean
reservedNameResolution.lean
resolveLVal.lean
returnOptIssue.lean
revert1.lean
revertMetavarKind.lean
rewrite.lean
rewrites.lean
rflApplyFoApprox.lean
rflProofsCongrCastsIssue.lean
rflReducibility.lean
rflTacticErrors.lean
robinson.lean
root.lean
rossel1.lean
run_cmd.lean
run_meta1.lean
rw_inst_implicit_args.lean
rw_inst_mvars.lean
rwRegression.lean
rwWithElabError.lean fix: make rewrite/rw tactic abort on elaboration errors (#6891) 2025-02-04 14:40:11 +00:00
safeExp.lean feat: asynchronous kernel checking 2025-01-23 19:07:31 -07:00
sarray.lean
scc.lean
scopedCommandAfterOpen.lean
scopedHindingIssue.lean
scopedLocalReducibility.lean
scopedParsers.lean
scopedParsers2.lean
scopedunifhint.lean
sealCommand.lean
secVarBug.lean
set.lean
set_lit_unexpand.lean
setOptionTermTactic.lean
setStructInstNotation.lean
seval1.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
sharecommon.lean
show_term.lean
showTests.lean
shrinkFn.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
sigmaprec.lean
sign.lean
simp-elab-recover.lean
simp1.lean
simp2.lean
simp3.lean
simp4.lean
simp5.lean
simp6.lean
simp_all.lean
simp_all_contextual.lean
simp_arith_deprecated.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
simp_arith_issues.lean fix: simp +arith (#7515) 2025-03-17 03:11:48 +00:00
simp_cache_perf_issue.lean
simp_eqn_bug.lean
simp_failIfUnchanged.lean
simp_inst_implict_args.lean
simp_int_arith.lean feat: alignment of Int.ediv/fdiv/tdiv lemmas (#7319) 2025-03-04 10:41:01 +00:00
simp_nat_arith.lean feat: simp +arith sorts linear atoms (#7040) 2025-02-11 23:37:30 +00:00
simp_proj_transparency_issue.lean
simpArith1.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
simpArithCacheIssue.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
simpAtDefIssue.lean
simpAutoUnfold.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
simpBool.lean
simpBug.lean
simpCasesOnCtorBug.lean
simpCnstr1.lean fix: simp +arith (#7515) 2025-03-17 03:11:48 +00:00
simpCondLemma.lean
simpConfigPropagationIssue1.lean
simpConfigPropagationIssue3.lean feat: make structure parent projections nameable (#7100) 2025-02-18 07:38:13 +00:00
simpDecide.lean
simpDefToUnfold.lean
simpDiag.lean refactor: WF: create unfold theorems eagerly (#6898) 2025-02-03 09:05:22 +00:00
simpDischargeLoop.lean
simpExpBlowup.lean
simpExtraArgsBug.lean
simpGround1.lean
simpHigherOrder.lean
simpIfPre.lean
simpImpLocal.lean
simpIndexDiag.lean
simpInv.lean
simpIssue.lean
simpJpCasesDepBug.lean
simpLetFunIssue.lean
simpLoopBug.lean
simpMatch.lean
simpMatchDiscr.lean
simpMatchDiscrIssue.lean
simpMatchEta.lean refactor: simpMatch to not etaStruct (#6901) 2025-02-01 19:04:05 +00:00
simpOnly.lean
simpPartialApp.lean
simpPreIssue.lean
simpPreprocess.lean
simpPrio.lean
simproc1.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
simproc2.lean
simproc_builtin_erase.lean
simproc_disable_issue.lean
simproc_erase.lean
simproc_panic.lean
simproc_timeout.lean
simprocFin.lean
simprocNat.lean fix: fix builtin simproc Nat.reduceAnd (#6773) 2025-01-25 12:57:24 +00:00
simprocSInt.lean feat: finite type conversions (Nat/Int/Fin/BitVec -> IntX -> *) (#7368) 2025-03-10 05:53:41 +00:00
simprocUInt.lean feat: IntX simprocs (#7228) 2025-03-03 13:37:57 +00:00
simpRwBug.lean
simpSInt.lean feat: finite type conversions (Nat/Int/Fin/BitVec -> IntX -> *) (#7368) 2025-03-10 05:53:41 +00:00
simpStar.lean
simpStarHyp.lean
simpUnfoldAbbrev.lean
sint-abs.lean feat: IntX.abs (#7131) 2025-02-18 13:16:30 +00:00
sint_conversions.lean feat: missing conversion functions for ISize (#7063) 2025-02-13 11:02:00 +00:00
sizeof1.lean
sizeof2.lean
sizeof3.lean
sizeof4.lean
sizeof5.lean
sizeof6.lean
skipAssignedInstances.lean
skipKernelTC.lean
smartUnfoldingBug.lean
solve_by_elim.lean
som1.lean
sorry.lean
spec_issue.lean
specbug.lean
specialize1.lean
specialize2.lean chore: style 2022-03-11 16:12:46 -08:00
specialize3.lean
split1.lean
split2.lean
split3.lean
splitAtCode.lean
splitIfIssue.lean
splitIssue.lean
splitIssue2.lean
splitList.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
splitOrderIssue.lean
starsAndBars.lean
state8.lean
state12.lean
stateRef.lean
streamEqIssue.lean
string.lean
string_gaps.lean
string_simprocs.lean
strInterpolation.lean chore: use #guard_msgs in run tests (#4175) 2024-05-16 00:38:31 +00:00
strLitProj.lean
struct1.lean
struct2.lean
struct3.lean feat: make structure parent projections nameable (#7100) 2025-02-18 07:38:13 +00:00
struct_inst_typed.lean
struct_instance_in_eqn.lean
structEqns.lean
structInst.lean
structInst2.lean
structInst3.lean
structInst4.lean
structInstFast.lean feat: make structure parent projections nameable (#7100) 2025-02-18 07:38:13 +00:00
structNamedParentProj.lean feat: make structure parent projections nameable (#7100) 2025-02-18 07:38:13 +00:00
structNoBody.lean
structPrivateFieldBug.lean
structPrivateFieldBug2.lean
structuralEqns.lean
structuralEqns2.lean
structuralEqns3.lean
structuralIssue.lean
structuralIssue2.lean
structuralMutual.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
structuralOverNested.lean
structuralRec1.lean
structuralRec2.lean feat: identify more fixed parameters (#7166) 2025-03-04 22:26:20 +00:00
structure.lean feat: split Lean.Kernel.Environment from Lean.Environment (#5145) 2025-01-18 18:42:57 +00:00
structure_recursive.lean chore: reimplement mk_projections in Lean (#7295) 2025-03-03 01:10:27 +00:00
structWithAlgTCSynth.lean feat: make structure parent projections nameable (#7100) 2025-02-18 07:38:13 +00:00
stuckMVarBug.lean
stuckTC.lean
stxKindInsideNamespace.lean
stxMacro.lean
subarray_split.lean
subarray_split.lean.expected.out
subexpr.lean
subscript_parser.lean fix: allow ⱼ in identifiers (#6679) 2025-01-21 03:51:51 +00:00
subset.lean
subst.lean
subst1.lean
substVars.lean
substWithoutExpectedType.lean
subtype_inj.lean
suffices.lean
symm.lean
syntax1.lean
syntaxAbbrevQuot.lean
syntaxPrio.lean
synth1.lean
synthInstsIssue.lean feat: make structure parent projections nameable (#7100) 2025-02-18 07:38:13 +00:00
synthOrderRegression.lean
synthPending1.lean
synthPendingBug.lean
tactic.lean
tactic1.lean
tactic_config.lean
tacticDoc.lean
tacticExtOverlap.lean
tacticTests.lean
takeSimpEqns.lean
task_test.lean
task_test2.lean chore: deprecate List.iota (#6708) 2025-01-21 02:32:35 +00:00
task_test_io.lean
taskState.lean feat: API to avoid deadlocks from dropped promises (#6958) 2025-02-07 15:33:10 +00:00
tc_eta_struct_issue.lean
tcUnivIssue.lean
tempfile.lean
termElab.lean
terminationByStructurally.lean refactor: TerminationArgument → TerminationMeasure (#6727) 2025-01-23 10:41:38 +00:00
termParserAttr.lean
TermSeq.lean
test_single.sh chore: run test suite with Elab.async for more coverage 2025-01-23 19:07:31 -07:00
thmIsProp.lean
time.lean
timeAPI.lean fix: negative timestamps and PlainDateTimes before 1970 (#6668) 2025-01-20 07:52:13 +00:00
timeClassOperations.lean
timeFormats.lean fix: adjustments to the datetime library (#6431) 2025-01-13 11:02:30 +00:00
timeIO.lean
timeLocalDateTime.lean
timeNegative.lean fix: negative timestamps and PlainDateTimes before 1970 (#6668) 2025-01-20 07:52:13 +00:00
timeOperations.lean
timeOperationsOffset.lean
timeParse.lean fix: negative timestamps and PlainDateTimes before 1970 (#6668) 2025-01-20 07:52:13 +00:00
timeSet.lean fix: adjustments to the datetime library (#6431) 2025-01-13 11:02:30 +00:00
timeTzifParse.lean
toArrayEq.lean
toDeclEtaBug.lean
toExpr.lean chore: remove functions for compiling decls from Environment (#6600) 2025-01-13 18:51:06 +00:00
toFromJson.lean
toLCNFCacheBug.lean
trace.lean
traceElabIssue.lean
traceFormat.lean fix: be consistent in not reporting newlines between trace nodes to info view (#7143) 2025-02-25 16:16:35 +00:00
trackZetaDeltaCacheIssue.lean
trans.lean chore: fix test 2021-08-25 07:00:25 -07:00
treemap.lean feat: more tree map lemmas about empty, isEmpty, contains, size, insert, erase (#7161) 2025-02-20 15:33:41 +00:00
treeNode.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
trivial_uint.lean feat: Neg instance for unsigned integers (#7487) 2025-03-17 09:06:14 +00:00
tryHeuristicPerfIssue.lean
tryHeuristicPerfIssue2.lean
tryPostponeIssue.lean
type_class_performance1.lean
typeAscImp.lean
typeclass_append.lean
typeclass_coerce.lean
typeclass_diamond.lean
typeclass_easy.lean
typeclass_loop.lean
typeclass_metas_internal_goals1.lean
typeclass_metas_internal_goals2.lean
typeclass_metas_internal_goals3.lean
typeclass_metas_internal_goals4.lean
typeclass_outparam.lean
typeOccursCheckIssue.lean
ubscalar.lean
unexpected_result_with_bind.lean
unfoldLemma.lean
unfoldMany.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
unfoldPartialRegression.lean
unfoldr.lean
unfoldTactic.lean
unif_issue.lean
unif_issue2.lean
unifhint1.lean
unifhint2.lean
unifhint3.lean
unihint.lean
univCnstrApprox.lean
univIssue.lean
univParamIssue.lean
univPolyEnum.lean
unsafeConst.lean
unsafeInit.lean
unsafeTerm.lean
update.lean
utf8英語.lean
varBinderUpdate.lean feat: allow updating binders to and from strict- and instance-implicit (#6634) 2025-02-05 15:43:54 +00:00
variable.lean feat: elaborate theorem bodies in parallel (#7084) 2025-03-14 07:50:42 +00:00
wf_preprocess.lean feat: propagate wfParam through let (#7039) 2025-02-12 13:22:08 +00:00
wf_preprocess_leak.lean feat: nested well-founded recursion via automatic preprocessing (#6744) 2025-02-10 16:43:41 +00:00
wfEqns1.lean
wfEqns2.lean
wfEqns3.lean
wfEqns4.lean
wfEqns5.lean
wfEqnsIssue.lean
wfForIn.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
wfirred.lean
wfLean3Issue.lean
wfOmega.lean
wfOverapplicationIssue.lean
wfrecUnary.lean
WFRelSearch.lean
wfSum.lean
wfUnfold.lean refactor: WF: create unfold theorems eagerly (#6898) 2025-02-03 09:05:22 +00:00
wfWithSidecondition.lean feat: nested well-founded recursion via automatic preprocessing (#6744) 2025-02-10 16:43:41 +00:00
where1.lean
whereCmd.lean
whileRepeat.lean
whnfDelayedMVarIssue.lean
WindowsNewlines.lean
withReducibleAndInstancesCrash.lean
zeroExitPoints.lean
zetaDelta.lean
zetaDeltaFalseDefEqIssue.lean
zetaDeltaIssue.lean
zetaDeltaSet.lean
zetaDeltaTryThisIssue.lean
zetaDSimpIssue.lean chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
zetaUnused.lean feat: zetaUnused option (implementation) (#6755) 2025-01-26 11:14:12 +00:00