| .. |
|
.gitattributes
|
chore: ensure consistent (Unix) encoding for source files
|
2023-03-10 16:27:56 +01:00 |
|
.gitignore
|
feat: IO.FS.Handle.lock/tryLock/unlock
|
2023-11-15 19:31:08 -05:00 |
|
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
|
feat: enable failIfUnchanged by default in simp
|
2023-08-16 10:14:23 -07:00 |
|
382.lean
|
|
|
|
387.lean
|
feat: enable failIfUnchanged by default in simp
|
2023-08-16 10:14:23 -07:00 |
|
394.lean
|
|
|
|
436.lean
|
|
|
|
436_lean3.lean
|
|
|
|
441.lean
|
|
|
|
447_lean3.lean
|
|
|
|
452.lean
|
|
|
|
457.lean
|
|
|
|
461a.lean
|
|
|
|
461b.lean
|
|
|
|
462.lean
|
|
|
|
463.lean
|
feat: use supplied structure fields left to right and eta reduce terms in structure instance elaboration (#2478)
|
2024-02-01 03:42:39 +00:00 |
|
470_lean3.lean
|
|
|
|
471.lean
|
|
|
|
474_lean3.lean
|
|
|
|
481.lean
|
|
|
|
482.lean
|
|
|
|
492.lean
|
fix: only return new mvars from refine, elabTermWithHoles, and withCollectingNewGoalsFrom (#2502)
|
2023-09-21 14:23:27 +10:00 |
|
492_lean3.lean
|
|
|
|
498.lean
|
|
|
|
500_lean3.lean
|
|
|
|
501.lean
|
|
|
|
509.lean
|
|
|
|
536.lean
|
|
|
|
561.lean
|
|
|
|
569.lean
|
|
|
|
602.lean
|
feat: reorder tc subgoals according to out-params
|
2023-04-10 13:00:04 -07:00 |
|
616.lean
|
|
|
|
633.lean
|
|
|
|
644.lean
|
|
|
|
646.lean
|
|
|
|
654.lean
|
|
|
|
664.lean
|
|
|
|
677.lean
|
|
|
|
696.lean
|
|
|
|
716.lean
|
|
|
|
753.lean
|
|
|
|
760.lean
|
|
|
|
764.lean
|
|
|
|
783.lean
|
|
|
|
788.lean
|
|
|
|
790.lean
|
|
|
|
793.lean
|
|
|
|
796.lean
|
chore: fix tests
|
2024-02-18 14:14:55 -08:00 |
|
815.lean
|
|
|
|
821.lean
|
|
|
|
837.lean
|
|
|
|
847.lean
|
|
|
|
854.lean
|
|
|
|
860.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
879.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
891.lean
|
chore: change simp default to decide := false (#2722)
|
2023-11-02 10:06:38 +11:00 |
|
909.lean
|
chore: fix more typos in comments
|
2023-10-08 14:37:34 -07:00 |
|
944.lean
|
|
|
|
945.lean
|
|
|
|
946.lean
|
|
|
|
955.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
968.lean
|
chore: upstream Std.Logic (#3312)
|
2024-02-14 09:40:55 +00:00 |
|
972.lean
|
|
|
|
974.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
983.lean
|
|
|
|
986.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
988.lean
|
|
|
|
998.lean
|
|
|
|
998Export.lean
|
|
|
|
1016.lean
|
|
|
|
1017.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
1018.lean
|
|
|
|
1020.lean
|
|
|
|
1022.lean
|
|
|
|
1024.lean
|
|
|
|
1025.lean
|
|
|
|
1026.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
1029.lean
|
|
|
|
1030.lean
|
|
|
|
1037.lean
|
|
|
|
1051.lean
|
|
|
|
1058.lean
|
|
|
|
1074a.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
1080.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
1113b.lean
|
|
|
|
1118.lean
|
|
|
|
1120.lean
|
|
|
|
1123.lean
|
|
|
|
1124.lean
|
|
|
|
1127.lean
|
|
|
|
1132.lean
|
|
|
|
1143.lean
|
|
|
|
1155.lean
|
|
|
|
1156.lean
|
|
|
|
1158.lean
|
|
|
|
1168.lean
|
|
|
|
1169.lean
|
|
|
|
1171.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
1179b.lean
|
|
|
|
1182.lean
|
|
|
|
1184.lean
|
|
|
|
1192.lean
|
|
|
|
1193a.lean
|
|
|
|
1193b.lean
|
|
|
|
1194.lean
|
|
|
|
1200.lean
|
|
|
|
1202.lean
|
feat: cleanups to ACI and Identity classes (#3195)
|
2024-01-24 21:46:58 +00:00 |
|
1224.lean
|
|
|
|
1228.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
1230.lean
|
|
|
|
1234.lean
|
|
|
|
1236.lean
|
|
|
|
1237.lean
|
|
|
|
1247.lean
|
|
|
|
1253.lean
|
|
|
|
1267.lean
|
|
|
|
1274.lean
|
|
|
|
1289.lean
|
|
|
|
1293.lean
|
chore: change simp default to decide := false (#2722)
|
2023-11-02 10:06:38 +11:00 |
|
1299.lean
|
|
|
|
1300.lean
|
|
|
|
1302.lean
|
chore: upstream Std.Data.Fin.Init.Lemmas (#3337)
|
2024-02-15 01:50:47 +00:00 |
|
1305.lean
|
|
|
|
1308.lean
|
|
|
|
1311.lean
|
|
|
|
1333.lean
|
|
|
|
1337.lean
|
feat: custom eliminators for induction and cases tactics, and beautiful eliminators for Nat (#3629)
|
2024-03-09 15:31:51 +00:00 |
|
1342.lean
|
|
|
|
1359.lean
|
|
|
|
1360.lean
|
|
|
|
1361.lean
|
|
|
|
1361b.lean
|
|
|
|
1365.lean
|
|
|
|
1372.lean
|
|
|
|
1373.lean
|
|
|
|
1374.lean
|
|
|
|
1375.lean
|
|
|
|
1380.lean
|
chore: upstream (most of) Std.Data.Nat.Lemmas (#3391)
|
2024-02-19 03:47:49 +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
|
chore: upstream Std.Logic (#3312)
|
2024-02-14 09:40:55 +00:00 |
|
1558.lean
|
|
|
|
1575.lean
|
|
|
|
1615.lean
|
|
|
|
1650.lean
|
|
|
|
1674.lean
|
|
|
|
1679.lean
|
|
|
|
1684.lean
|
|
|
|
1686.lean
|
|
|
|
1692.lean
|
|
|
|
1711.lean
|
feat: enable failIfUnchanged by default in simp
|
2023-08-16 10:14:23 -07:00 |
|
1725.lean
|
|
|
|
1730.lean
|
|
|
|
1780.lean
|
|
|
|
1787.lean
|
|
|
|
1808.lean
|
|
|
|
1812.lean
|
|
|
|
1813.lean
|
fix: calc indentation and allow underscore in first relation
|
2023-02-23 14:20:21 -08:00 |
|
1815.lean
|
|
|
|
1822.lean
|
|
|
|
1829.lean
|
|
|
|
1841.lean
|
|
|
|
1842.lean
|
chore: upstream Std.Logic (#3312)
|
2024-02-14 09:40:55 +00:00 |
|
1848.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
1850.lean
|
|
|
|
1851.lean
|
|
|
|
1852.lean
|
fix: include instance implicits that depend on outParams at outParamsPos
|
2022-12-01 06:11:48 -08:00 |
|
1869.lean
|
|
|
|
1882.lean
|
|
|
|
1883.lean
|
|
|
|
1886.lean
|
|
|
|
1892.lean
|
|
|
|
1900.lean
|
fix: fixes #1900
|
2022-12-02 10:04:01 -08:00 |
|
1901.lean
|
feat: reorder tc subgoals according to out-params
|
2023-04-10 13:00:04 -07:00 |
|
1907.lean
|
fix: fixes #1907
|
2022-12-02 08:59:16 -08:00 |
|
1907orig.lean
|
fix: fixes #1907
|
2022-12-02 08:59:16 -08:00 |
|
1921.lean
|
chore: change simp default to decide := false (#2722)
|
2023-11-02 10:06:38 +11:00 |
|
1926.lean
|
feat: use forall_prop_domain_congr in simp tactic
|
2023-10-23 06:19:19 -07:00 |
|
1937.lean
|
test: for issue #1937
|
2023-01-05 13:46:15 -08:00 |
|
1951.lean
|
refactor: replace ignoreLevelMVarDepth by levelAssignDepth
|
2022-12-19 20:14:17 +01:00 |
|
1954.lean
|
|
|
|
1963.lean
|
fix: implement assertAfter using revert
|
2022-12-21 21:42:07 +01:00 |
|
1968.lean
|
|
|
|
1985.lean
|
fix: correctly parse json unicode escapes
|
2022-12-23 17:04:10 -08:00 |
|
1986.lean
|
perf: whnf projections during defeq
|
2023-02-09 19:54:23 -08:00 |
|
2009.lean
|
fix: fixes #2009
|
2023-01-04 10:32:03 -08:00 |
|
2018.lean
|
fix: add done alternative to decreasing_with (#2019)
|
2023-01-09 09:46:37 -08:00 |
|
2042.lean
|
fix: fixes #2042
|
2023-11-09 04:06:30 -08:00 |
|
2073.lean
|
chore: add test for calc
|
2023-02-21 16:41:46 -08:00 |
|
2074.lean
|
chore: remove etaExperiment option
|
2023-05-15 09:05:41 -07:00 |
|
2079.lean
|
fix: calc: synthesize default instances
|
2023-02-02 14:29:21 -08:00 |
|
2095.lean
|
fix: unify goal before executing nested tactics in calc
|
2023-02-09 11:34:07 -08:00 |
|
2136.lean
|
fix: offset unification with a+a+1
|
2023-05-15 09:06:37 -07:00 |
|
2137.lean
|
fix: do not inherit file handles across process creation
|
2023-03-10 16:27:56 +01:00 |
|
2159.lean
|
fix: ofScientific at simp (#3628)
|
2024-03-07 00:11:31 +00:00 |
|
2173.lean
|
fix: simp: strip mdata when testing for True/False
|
2023-04-10 21:06:42 -07:00 |
|
2182.lean
|
chore: add missing simp lemma (¬ False) = True
|
2023-04-10 21:05:54 -07:00 |
|
2188.lean
|
fix: reset local context in mkInjectiveTheorems
|
2023-04-10 21:05:16 -07:00 |
|
2199.lean
|
fix: fixes #2199
|
2023-05-28 18:29:09 -07:00 |
|
2243.lean
|
fix: an equation lemma with autoParam arguments fails to rewrite (#3316)
|
2024-02-17 13:42:34 +00:00 |
|
2249.lean
|
fix: prefer resolving parser alias over declaration
|
2023-06-05 16:52:23 +02:00 |
|
2262.lean
|
fix: hygieneInfo should not consume whitespace
|
2023-06-09 15:05:19 +02:00 |
|
2265.lean
|
fix: simp: synthesize non-inst-implicit tc args
|
2023-06-09 16:32:02 -07:00 |
|
2282.lean
|
fix: fixes #2282
|
2023-06-27 16:46:38 -07:00 |
|
2299.lean
|
chore: write "|-" as "|" noWs "-" (#2299)
|
2023-07-14 09:48:20 -07:00 |
|
2311.lean
|
feat: relax test in checkLocalInstanceParameters to allow instance implicits
|
2023-07-13 10:54:06 -07:00 |
|
2344.lean
|
fix: missing mkCIdents in Lean.Elab.Deriving.Util
|
2023-07-28 07:48:34 -07:00 |
|
2389.lean
|
fix: don't try to generate below for nested predicates. (#2390)
|
2023-09-21 14:24:37 +10:00 |
|
2389.lean.expected.out
|
fix: don't try to generate below for nested predicates. (#2390)
|
2023-09-21 14:24:37 +10:00 |
|
2500.lean
|
fix : make mk_no_confusion_type handle delta-reduction when generating telescope (#2501)
|
2023-10-14 17:18:37 +11:00 |
|
2552.lean
|
chore: upstream Std.Logic (#3312)
|
2024-02-14 09:40:55 +00:00 |
|
2615.lean
|
refactor: Offset.lean and related files (#3614)
|
2024-03-05 19:40:15 -08:00 |
|
2669.lean
|
chore: fix tests
|
2024-02-18 14:14:55 -08:00 |
|
2670.lean
|
feat: assume function application arguments occurring in local simp theorems have been annotated with no_index (#3406)
|
2024-02-19 12:43:34 -08:00 |
|
2672.lean
|
fix: quot reduction bug
|
2023-10-11 21:25:34 -07:00 |
|
2810.lean
|
fix: predefinition preprocessing: float .mdata out of non-unary applications (#3204)
|
2024-01-24 08:37:16 +00:00 |
|
2835.lean
|
test: issue #2835
|
2024-03-06 15:29:04 -08:00 |
|
2843.lean
|
test: for issue #2843
|
2024-02-18 14:14:55 -08:00 |
|
2846.lean
|
fix: make delabConstWithSignature avoid using inaccessible names (#3625)
|
2024-03-07 18:14:06 +00:00 |
|
2862.lean
|
fix: simp gets stuck on autoParam (#3315)
|
2024-02-17 13:42:19 +00:00 |
|
2914.lean
|
fix: DecidableEq deriving handler could not handle fields whose types start with an implicit argument (#2918)
|
2023-11-20 20:51:47 +11:00 |
|
2916.lean
|
fix: fold raw Nat literals at dsimp (#3624)
|
2024-03-06 18:29:20 +00:00 |
|
2939.lean
|
fix: an equation lemma with autoParam arguments fails to rewrite (#3316)
|
2024-02-17 13:42:34 +00:00 |
|
2966.lean
|
chore: update tests for #2966 to use test_extern (#3092)
|
2023-12-21 22:22:47 +00:00 |
|
3022.lean
|
feat: better support for reducing Nat.rec (#3616)
|
2024-03-06 13:28:07 +00:00 |
|
3229.lean
|
fix: cache issue at split tatic (#3258)
|
2024-02-06 19:44:28 +00:00 |
|
3242.lean
|
fix: instantiate the types of inductives with the right parameters (#3246)
|
2024-02-17 16:52:28 +00:00 |
|
3257.lean
|
fix: simp fails to discharge autoParam premises even when it can reduce them to True (#3314)
|
2024-02-17 13:41:48 +00:00 |
|
3395.lean
|
fix: dsimp should reduce kernel projections (#3607)
|
2024-03-05 14:56:27 +00:00 |
|
3501.lean
|
fix: simp? should track unfolded let-decls (#3510)
|
2024-02-26 20:49:24 +00:00 |
|
3519.lean
|
fix: simp trace issues (#3522)
|
2024-02-27 23:19:25 +00:00 |
|
3524.lean
|
fix: generalize excessive resource usage (#3575)
|
2024-03-03 17:58:11 +00:00 |
|
3547.lean
|
fix: simp? suggests generated equations lemma names (#3573)
|
2024-03-02 23:59:35 +00:00 |
|
abstractExpr.lean
|
|
|
|
ac_expr.lean
|
|
|
|
ac_rfl.lean
|
chore: add @[simp] to Nat.succ_eq_add_one, and cleanup downstream (#3579)
|
2024-03-13 05:35:52 +00:00 |
|
ack.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
ACltBug.lean
|
|
|
|
adam1.lean
|
|
|
|
adamTC.lean
|
|
|
|
adamTC2.lean
|
|
|
|
add_suggestion.lean
|
chore: begin moving orphaned tests from Std
|
2024-02-29 10:54:19 +11:00 |
|
addDecorationsWithoutPartial.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
alex1.lean
|
|
|
|
alg.lean
|
|
|
|
alias.lean
|
|
|
|
allGoals.lean
|
|
|
|
and_intros.lean
|
chore: upstream repeat/split_ands/subst_eqs (#3305)
|
2024-02-13 12:21:14 +00:00 |
|
andCasesOnBug.lean
|
|
|
|
anonymous_ctor_error_msg.lean
|
|
|
|
anonymousCtor.lean
|
|
|
|
appFinalizeIssue.lean
|
|
|
|
appIssue.lean
|
|
|
|
apply_tac.lean
|
|
|
|
apply_tac.lean.expected.out
|
|
|
|
applytransp.lean
|
|
|
|
approxDepth.lean
|
|
|
|
array1.lean
|
|
|
|
arrowDot.lean
|
|
|
|
arthur1.lean
|
chore: upstream Std.Data.Bool (#3389)
|
2024-02-19 02:44:07 +00:00 |
|
arthur2.lean
|
chore: upstream Std.Data.Bool (#3389)
|
2024-02-19 02:44:07 +00:00 |
|
assertAfterBug.lean
|
|
|
|
aStructPerfIssue.lean
|
feat: custom eliminators for induction and cases tactics, and beautiful eliminators for Nat (#3629)
|
2024-03-09 15:31:51 +00:00 |
|
attachJp.lean
|
|
|
|
autoboundIssues.lean
|
|
|
|
autoLift.lean
|
|
|
|
autoLiftIssue.lean
|
|
|
|
autoparam.lean
|
|
|
|
backtrackable_estate.lean
|
|
|
|
balg.lean
|
|
|
|
bigctor.lean
|
|
|
|
bigmul.lean
|
|
|
|
bigop.lean
|
|
|
|
bindCasesIssue.lean
|
|
|
|
binderNotation.lean
|
|
|
|
binrec.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
binrel.lean
|
|
|
|
binrelmacros.lean
|
|
|
|
bitvec.lean
|
chore: begin moving orphaned tests from Std
|
2024-02-29 10:54:19 +11:00 |
|
bitvec_fin_literal_norm.lean
|
chore: move BitVec to top level namespace
|
2024-02-23 15:15:57 -08:00 |
|
bitvec_simproc.lean
|
chore: move BitVec to top level namespace
|
2024-02-23 15:15:57 -08:00 |
|
borrowBug.lean
|
|
|
|
bubble.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
bugNatLitDiscrTree.lean
|
fix: Nat literal bug at DiscrTree.lean
|
2023-06-21 20:28:17 -07:00 |
|
bv_math_lit_perf.lean
|
perf: mkSplitterProof
|
2024-02-24 16:08:07 -08:00 |
|
by_cases.lean
|
chore: upstream Std.Tactic.ByCases
|
2024-02-09 09:57:57 +11:00 |
|
byteSliceIssue.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
calc.lean
|
fix: calc indentation and allow underscore in first relation
|
2023-02-23 14:20:21 -08:00 |
|
calcBug.lean
|
fix: calc indentation and allow underscore in first relation
|
2023-02-23 14:20:21 -08:00 |
|
calcInType.lean
|
|
|
|
casePrime.lean
|
|
|
|
casesAnyTypeIssue.lean
|
feat: custom eliminators for induction and cases tactics, and beautiful eliminators for Nat (#3629)
|
2024-03-09 15:31:51 +00:00 |
|
casesRec.lean
|
|
|
|
casesUsing.lean
|
|
|
|
catchThe.lean
|
|
|
|
cdotTests.lean
|
|
|
|
change.lean
|
chore: begin moving orphaned tests from Std
|
2024-02-29 10:54:19 +11:00 |
|
change_tac.lean
|
chore: upstream change tactic (#3308)
|
2024-02-13 04:47:11 +00:00 |
|
check.lean
|
|
|
|
check_failure.lean
|
|
|
|
checkAssignmentIssue.lean
|
|
|
|
choiceExpectedTypeBug.lean
|
|
|
|
choiceMacroRules.lean
|
|
|
|
class_inductive.lean
|
|
|
|
classAbbrev.lean
|
|
|
|
closure1.lean
|
|
|
|
codeBindUnreachIssue.lean
|
|
|
|
coeIssue1.lean
|
|
|
|
coeIssue2.lean
|
|
|
|
coeIssue3.lean
|
|
|
|
coeIssues4.lean
|
|
|
|
coelambda.lean
|
|
|
|
CoeNew.lean
|
|
|
|
coeOutParamIssue.lean
|
|
|
|
coeOutParamIssue2.lean
|
|
|
|
coeSort1.lean
|
|
|
|
coeSort2.lean
|
|
|
|
combinatorsAndWF.lean
|
|
|
|
CommandExtOverlap.lean
|
|
|
|
compatibleTypesBugAtLCNF.lean
|
|
|
|
compatibleTypesEtaIssue.lean
|
feat: custom eliminators for induction and cases tactics, and beautiful eliminators for Nat (#3629)
|
2024-03-09 15:31:51 +00:00 |
|
compiler_erase_bug.lean
|
|
|
|
compiler_proj_bug.lean
|
|
|
|
CompilerCSE.lean
|
|
|
|
CompilerFindJoinPoints.lean
|
|
|
|
CompilerFloatLetIn.lean
|
|
|
|
CompilerProbe.lean
|
|
|
|
CompilerPullInstances.lean
|
|
|
|
CompilerSimp.lean
|
|
|
|
compilerTest1.lean
|
|
|
|
computedFields.lean
|
|
|
|
concatElim.lean
|
chore: upstream (most of) Std.Data.Nat.Lemmas (#3391)
|
2024-02-19 03:47:49 +00:00 |
|
congrTactic.lean
|
|
|
|
congrThm.lean
|
|
|
|
constantCompilerBug.lean
|
|
|
|
constFun.lean
|
|
|
|
constFun2.lean
|
|
|
|
constProp.lean
|
chore: upstream NatCast and IntCast (#3347)
|
2024-02-16 00:54:22 +00:00 |
|
contra.lean
|
feat: type of theorems must be propositions
|
2024-03-13 12:37:58 -07:00 |
|
contradiction1.lean
|
|
|
|
contradictionExfalso.lean
|
|
|
|
contradictionLoop.lean
|
|
|
|
conv1.lean
|
|
|
|
conv2.lean
|
|
|
|
convcalc.lean
|
feat: conv => calc (#3659)
|
2024-03-13 09:03:39 +00:00 |
|
core.lean
|
|
|
|
crashDiv0.lean
|
|
|
|
csimp_type_error.lean
|
|
|
|
csimpAttrFn.lean
|
|
|
|
ctorAutoParams.lean
|
|
|
|
Daniel1.lean
|
|
|
|
deBruijn.lean
|
|
|
|
decAuxBug.lean
|
|
|
|
decClassical.lean
|
|
|
|
decEq.lean
|
|
|
|
decidability_timeout.lean
|
chore: upstream orphaned tests from Std (#3539)
|
2024-02-29 04:12:52 +00:00 |
|
decidelet.lean
|
|
|
|
declareConfigElabBug.lean
|
feat: enable failIfUnchanged by default in simp
|
2023-08-16 10:14:23 -07:00 |
|
declareConfigElabIssue.lean
|
|
|
|
decreasingTacticUpdatedEnvIssue.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
deep1.lean
|
|
|
|
def1.lean
|
|
|
|
def2.lean
|
|
|
|
def3.lean
|
|
|
|
def4.lean
|
|
|
|
def5.lean
|
|
|
|
def6.lean
|
|
|
|
def7.lean
|
|
|
|
def8.lean
|
|
|
|
def9.lean
|
|
|
|
def10.lean
|
chore: change simp default to decide := false (#2722)
|
2023-11-02 10:06:38 +11:00 |
|
def11.lean
|
|
|
|
def12.lean
|
|
|
|
def13.lean
|
|
|
|
def14.lean
|
|
|
|
def15.lean
|
|
|
|
def16.lean
|
|
|
|
def17.lean
|
|
|
|
def18.lean
|
|
|
|
def19.lean
|
|
|
|
def20.lean
|
|
|
|
defaultEliminator.lean
|
feat: custom eliminators for induction and cases tactics, and beautiful eliminators for Nat (#3629)
|
2024-03-09 15:31:51 +00:00 |
|
defaultInstBacktrackIssue.lean
|
|
|
|
defaulValueParamIssue.lean
|
|
|
|
DefEqAssignBug.lean
|
|
|
|
defEqVsWhnfI.lean
|
|
|
|
depElim1.lean
|
fix: regression on match expressions with builtin literals (#3521)
|
2024-02-27 18:49:44 +00:00 |
|
depFieldIssue.lean
|
|
|
|
depHd.lean
|
|
|
|
deq.lean
|
chore: rwa tactic macro (#3299)
|
2024-02-10 04:59:24 +00:00 |
|
deriv.lean
|
|
|
|
derivingBEq.lean
|
|
|
|
derivingHashable.lean
|
|
|
|
derivingInhabited.lean
|
|
|
|
derivingNonempty.lean
|
feat: add derive handler for Nonempty
|
2022-12-22 03:48:15 +01:00 |
|
diamond1.lean
|
|
|
|
diamond2.lean
|
|
|
|
diamond3.lean
|
|
|
|
diamond4.lean
|
|
|
|
diamond5.lean
|
|
|
|
discrRefinement.lean
|
|
|
|
discrRefinement2.lean
|
feat: type of theorems must be propositions
|
2024-03-13 12:37:58 -07:00 |
|
discrRefinement3.lean
|
|
|
|
discrTreeOffset.lean
|
|
|
|
discrTreeSimp.lean
|
chore: fix tests
|
2023-11-09 04:06:30 -08:00 |
|
do_eqv.lean
|
|
|
|
do_eqv_proofs.lean
|
|
|
|
doElemAsTermNotation.lean
|
|
|
|
dofun_prec.lean
|
|
|
|
doLetElse.lean
|
fix: allow generalization in let (#3060)
|
2024-01-23 09:02:05 +00:00 |
|
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
|
|
|
|
dsimp_bv_simproc.lean
|
feat: use dsimprocs at dsimp
|
2024-03-05 14:42:05 -08:00 |
|
dsimproc.lean
|
feat: use dsimprocs at dsimp
|
2024-03-05 14:42:05 -08:00 |
|
DVec.lean
|
|
|
|
dynamic.lean
|
|
|
|
eagerInliningIssue.lean
|
|
|
|
elab_cmd.lean
|
|
|
|
elabCmd.lean
|
|
|
|
elabIte.lean
|
|
|
|
eliminatorImplicitTargets.lean
|
feat: custom eliminators for induction and cases tactics, and beautiful eliminators for Nat (#3629)
|
2024-03-09 15:31:51 +00:00 |
|
elimOptParam.lean
|
fix: bug at elimOptParam (#3595)
|
2024-03-04 23:56:00 +00:00 |
|
elseCaseArrow.lean
|
|
|
|
elseIfConfusion.lean
|
|
|
|
emptycOverloadIssues.lean
|
|
|
|
emptyLcnf.lean
|
|
|
|
enumDecEq.lean
|
|
|
|
enumNoConfusionIssue.lean
|
|
|
|
eq_some_iff_get_eq_issue.lean
|
chore: upstream Option material from Std (#3356)
|
2024-02-16 02:05:18 +00:00 |
|
eqndrecEtaLCNFIssue.lean
|
|
|
|
eqnsAtSimp.lean
|
chore: add @[simp] to Nat.succ_eq_add_one, and cleanup downstream (#3579)
|
2024-03-13 05:35:52 +00:00 |
|
eqnsAtSimp2.lean
|
chore: add @[simp] to Nat.succ_eq_add_one, and cleanup downstream (#3579)
|
2024-03-13 05:35:52 +00:00 |
|
eqnsAtSimp3.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
eqTheoremForVec.lean
|
chore: upstream (most of) Std.Data.Nat.Lemmas (#3391)
|
2024-02-19 03:47:49 +00:00 |
|
eqThm.lean
|
|
|
|
eqThmWithMoreThanOneAsPattern.lean
|
|
|
|
eqValue.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
erased.lean
|
|
|
|
eraseSuffix.lean
|
|
|
|
erasureConfusion.lean
|
|
|
|
etaFirst.lean
|
|
|
|
etaStruct.lean
|
|
|
|
etaStructProofIrrelIssue.lean
|
chore: upstream Std.BitVec.* (#3400)
|
2024-02-19 12:43:34 -08:00 |
|
eval_unboxed_const.lean
|
|
|
|
evalBuiltinInit.lean
|
|
|
|
evalconst.lean
|
|
|
|
evalDo.lean
|
|
|
|
evalInit.lean
|
|
|
|
evalProp.lean
|
|
|
|
evalTacticBug.lean
|
|
|
|
exfalsoBug.lean
|
feat: enable failIfUnchanged by default in simp
|
2023-08-16 10:14:23 -07:00 |
|
exists.lean
|
|
|
|
exp.lean
|
|
|
|
expandAbbrevAtIsClass.lean
|
|
|
|
expandWhereStructInstIssue.lean
|
|
|
|
expectedTypePropagation.lean
|
|
|
|
explicitMotive.lean
|
|
|
|
explictOpenDeclIssue.lean
|
|
|
|
expr1.lean
|
|
|
|
expr_maps.lean
|
|
|
|
ExprLens.lean
|
|
|
|
ext.lean
|
chore: upstream orphaned tests from Std (#3539)
|
2024-02-29 04:12:52 +00:00 |
|
ext1.lean
|
chore: upstream Std.BitVec.* (#3400)
|
2024-02-19 12:43:34 -08:00 |
|
extensibleTacticBug.lean
|
|
|
|
extern.lean
|
|
|
|
extmacro.lean
|
|
|
|
falseElimAtSimpLocalDecl.lean
|
|
|
|
fieldAbbrevInPat.lean
|
|
|
|
fieldAutoBound.lean
|
|
|
|
fieldDefaultValueWithoutType.lean
|
|
|
|
fieldIssue.lean
|
|
|
|
fieldNamesWithMinus.lean
|
fix: support escaped field names in dot-notation
|
2022-12-02 03:48:19 +01:00 |
|
fieldTypeBug.lean
|
|
|
|
filter.lean
|
|
|
|
finally.lean
|
|
|
|
finDotCtor.lean
|
|
|
|
finLit.lean
|
fix: complete Fin match
|
2024-02-24 16:08:07 -08:00 |
|
finMatch.lean
|
|
|
|
flat_expr.lean
|
|
|
|
float1.lean
|
|
|
|
float_cases_bug.lean
|
|
|
|
float_from_bignum.lean
|
|
|
|
floatarray.lean
|
|
|
|
floatOptParam.lean
|
|
|
|
foApprox.lean
|
|
|
|
foldConsts.lean
|
|
|
|
foldLits.lean
|
feat: simprocs for folding numeric literals (#3586)
|
2024-03-04 02:51:04 +00:00 |
|
forBodyResultTypeIssue.lean
|
|
|
|
forInElabBug.lean
|
|
|
|
forInPArray.lean
|
|
|
|
forInRangeWF.lean
|
|
|
|
forInReturnPropagation.lean
|
|
|
|
forInUniv.lean
|
|
|
|
forOutParamIssue.lean
|
|
|
|
forParallel.lean
|
|
|
|
french_quote.lean
|
|
|
|
frontend_meeting_2022_09_13.lean
|
|
|
|
fun.lean
|
|
|
|
funext.lean
|
feat: funext no arg tactic (#2027)
|
2023-01-15 08:53:49 -08:00 |
|
funind_demo.lean
|
fix: make delabConstWithSignature avoid using inaccessible names (#3625)
|
2024-03-07 18:14:06 +00:00 |
|
funind_expr.lean
|
feat: functional induction (#3432)
|
2024-03-05 13:02:05 +00:00 |
|
funind_mutual_dep.lean
|
fix: make delabConstWithSignature avoid using inaccessible names (#3625)
|
2024-03-07 18:14:06 +00:00 |
|
funind_proof.lean
|
feat: functional induction (#3432)
|
2024-03-05 13:02:05 +00:00 |
|
funind_tests.lean
|
fix: make delabConstWithSignature avoid using inaccessible names (#3625)
|
2024-03-07 18:14:06 +00:00 |
|
funMatchIssue.lean
|
|
|
|
generalize.lean
|
|
|
|
generalizeMany.lean
|
|
|
|
generalizeTelescope.lean
|
|
|
|
genindices.lean
|
|
|
|
getline_crash.lean
|
|
|
|
guard_expr.lean
|
chore: upstream orphaned tests from Std (#3539)
|
2024-02-29 04:12:52 +00:00 |
|
guard_msgs.lean
|
feat: guard_msgs to escapes trailing newlines (#3617)
|
2024-03-12 16:35:14 +00:00 |
|
guardexpr.lean
|
feat: upstream guard_expr (#3297)
|
2024-02-11 23:25:04 +00:00 |
|
handleLocking.lean
|
feat: IO.FS.Handle.lock/tryLock/unlock
|
2023-11-15 19:31:08 -05:00 |
|
hashableBug.lean
|
|
|
|
haveDestruct.lean
|
|
|
|
haveI.lean
|
chore: builtin haveI and letI
|
2024-02-15 14:33:36 +11:00 |
|
haveTactic.lean
|
fix: make elabTermEnsuringType respect errToSorry when there is a type mismatch (#3633)
|
2024-03-09 15:30:47 +00:00 |
|
hcongr.lean
|
|
|
|
heapSort.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
heqSubst.lean
|
|
|
|
hlistOverload.lean
|
|
|
|
hmul2.lean
|
|
|
|
hmulDefaultIntance.lean
|
|
|
|
ifcongr.lean
|
|
|
|
iffRefl.lean
|
|
|
|
ifThenElseIssue.lean
|
|
|
|
ifThenElseIssue2.lean
|
|
|
|
impByNameResolution.lean
|
|
|
|
impLambdaTac.lean
|
|
|
|
implicitApplyIssue.lean
|
|
|
|
implicitLambdaLocalWithoutType.lean
|
|
|
|
implicitTypesRecCoe.lean
|
|
|
|
inaccessibleAnnotDefEqIssue.lean
|
chore: upstream Std.Data.Int.Init modules (#3364)
|
2024-02-16 03:58:23 +00:00 |
|
incmd.lean
|
|
|
|
ind_cmd_bug.lean
|
|
|
|
ind_whnf.lean
|
|
|
|
ind_whnf2.lean
|
|
|
|
induction1.lean
|
|
|
|
inductionAltExplicit.lean
|
|
|
|
inductionLetIssue.lean
|
chore: fix tests
|
2024-02-18 14:14:55 -08:00 |
|
inductionParse.lean
|
|
|
|
inductionTacticBug.lean
|
|
|
|
inductive1.lean
|
|
|
|
inductive2.lean
|
|
|
|
inductive_pred.lean
|
|
|
|
inductiveIndicesIssue.lean
|
|
|
|
indUsingLet.lean
|
fix: include let bindings when determining altParamNums for eliminators (#3505)
|
2024-02-28 13:14:34 +00:00 |
|
inferForallTypeLCNF.lean
|
|
|
|
infixprio.lean
|
|
|
|
inj1.lean
|
|
|
|
inj2.lean
|
feat: type of theorems must be propositions
|
2024-03-13 12:37:58 -07:00 |
|
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
|
|
|
|
inlineWithNestedRecIssue.lean
|
|
|
|
instanceIssues.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
instances.lean
|
chore: split up & simplify importModules
|
2023-08-31 15:37:33 -04:00 |
|
instanceWhere.lean
|
|
|
|
instanceWhereDecls.lean
|
|
|
|
instEtaIssue.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
instPatVar.lean
|
|
|
|
instprio.lean
|
|
|
|
instuniv.lean
|
chore: split up & simplify importModules
|
2023-08-31 15:37:33 -04:00 |
|
int_complement_shiftRight.lean
|
chore: upstream orphaned tests from Std (#3539)
|
2024-02-29 04:12:52 +00:00 |
|
int_to_nat_bug.lean
|
|
|
|
internalizeCasesIssue.lean
|
feat: custom eliminators for induction and cases tactics, and beautiful eliminators for Nat (#3629)
|
2024-03-09 15:31:51 +00:00 |
|
interp.lean
|
|
|
|
interp2.lean
|
|
|
|
introLetFun.lean
|
feat: make intro be aware of let_fun (#3115)
|
2024-01-31 08:55:52 +00:00 |
|
intromacro.lean
|
|
|
|
IO_test.lean
|
fix: use MoveFileEx for rename on win
|
2023-09-19 20:24:37 +02:00 |
|
ioRandomBytes.lean
|
|
|
|
irCompilerBug.lean
|
|
|
|
irreducibleIssue.lean
|
feat: reorder tc subgoals according to out-params
|
2023-04-10 13:00:04 -07:00 |
|
isDefEqCheckAssignmentBug.lean
|
|
|
|
isDefEqConstApproxIssue.lean
|
|
|
|
isDefEqIssue.lean
|
|
|
|
isDefEqMVarSelfIssue.lean
|
|
|
|
isDefEqPerfIssue.lean
|
|
|
|
isDefEqProjPerfIssue.lean
|
|
|
|
issue2628.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
issue2883.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
issue2925.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
issue2982.lean
|
test: termination checking and duplicated terms (#2993)
|
2023-11-29 15:40:57 +00:00 |
|
issue3175.lean
|
fix: Fix/GuessLex: refine through more casesOnApp/matcherApp (#3176)
|
2024-01-13 18:02:41 +00:00 |
|
issue3204.lean
|
fix: predefinition preprocessing: float .mdata out of non-unary applications (#3204)
|
2024-01-24 08:37:16 +00:00 |
|
issue3212.lean
|
fix: let induction handle parameters (#3256)
|
2024-02-06 20:32:12 +00:00 |
|
james1.lean
|
|
|
|
jason1.lean
|
|
|
|
json.lean
|
chore: upstream orphaned tests from Std (#3539)
|
2024-02-29 04:12:52 +00:00 |
|
kernel1.lean
|
|
|
|
kernel2.lean
|
|
|
|
kernelInterrupt.lean
|
fix: revert shared library split on non-Windows platforms (#3529)
|
2024-02-29 19:15:01 +00:00 |
|
kevin.lean
|
|
|
|
krivine.lean
|
|
|
|
kronRWIssue.lean
|
|
|
|
KyleAlg.lean
|
|
|
|
KyleAlgAbbrev.lean
|
|
|
|
lazyListRotateUnfoldProof.lean
|
feat: type of theorems must be propositions
|
2024-03-13 12:37:58 -07:00 |
|
lazylistThunk.lean
|
|
|
|
lazyUnfoldingPerfIssue.lean
|
chore: the previous commit exposed an issue with simp
|
2023-11-03 05:56:59 -07:00 |
|
lcnf1.lean
|
|
|
|
lcnf2.lean
|
|
|
|
lcnf3.lean
|
|
|
|
lcnf4.lean
|
|
|
|
lcnf_simp_let.lean
|
fix: LCNF simp forgot to mark normalized decls as simplified
|
2023-05-05 12:17:26 -07:00 |
|
lcnfBinderNameBug.lean
|
|
|
|
lcnfCastIssue.lean
|
feat: custom eliminators for induction and cases tactics, and beautiful eliminators for Nat (#3629)
|
2024-03-09 15:31:51 +00:00 |
|
lcnfCheckIssue.lean
|
|
|
|
lcnfEtaExpandBug.lean
|
|
|
|
lcnfInferProjTypeBug.lean
|
|
|
|
lcnfInferProjTypeIssue.lean
|
|
|
|
lcnfInliningIssue.lean
|
feat: custom eliminators for induction and cases tactics, and beautiful eliminators for Nat (#3629)
|
2024-03-09 15:31:51 +00:00 |
|
lcnfIssue.lean
|
|
|
|
lean3_zulip_issues_1.lean
|
|
|
|
lean_nat_bitwise.lean
|
feat: add bitwise operations to reduceNat? and kernel (#3134)
|
2024-01-11 18:12:45 +00:00 |
|
lean_nat_gcd.lean
|
feat: use nat_gcd in the kernel (#2533)
|
2023-10-15 13:49:41 +11:00 |
|
left_right.lean
|
chore: upstream orphaned tests from Std (#3539)
|
2024-02-29 04:12:52 +00:00 |
|
lemma.lean
|
feat: type of theorems must be propositions
|
2024-03-13 12:37:58 -07:00 |
|
let_Issue.lean
|
|
|
|
letBRecOnIssue.lean
|
|
|
|
letDeclSimp.lean
|
test: for simp [x] where x is a let-variable
|
2023-10-25 03:12:35 -07:00 |
|
letMVar.lean
|
|
|
|
letrecInProofs.lean
|
|
|
|
letrecInThm.lean
|
fix: auxiliary definition nested in theorem should be def if its type is not a proposition (#3662)
|
2024-03-13 09:38:37 +00:00 |
|
letrecWFIssue.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
level.lean
|
|
|
|
levelNamesInTacticMode.lean
|
|
|
|
levelNGen.lean
|
feat: type of theorems must be propositions
|
2024-03-13 12:37:58 -07:00 |
|
lex.lean
|
chore: upstream Option material from Std (#3356)
|
2024-02-16 02:05:18 +00:00 |
|
liftMethodInMacrosIssue.lean
|
|
|
|
LiftMethodIssue.lean
|
|
|
|
linearByRefl.lean
|
|
|
|
listDecEq.lean
|
|
|
|
listtostring.lean
|
fix: make List.toString tail-recursive
|
2022-12-12 22:58:21 +01:00 |
|
litToCtor.lean
|
fix: regression on match expressions with builtin literals (#3521)
|
2024-02-27 18:49:44 +00:00 |
|
localNameResolutionWithProj.lean
|
|
|
|
localParsers.lean
|
|
|
|
macro.lean
|
chore: upstream set notation (#3339)
|
2024-02-15 02:08:45 +00:00 |
|
macro2.lean
|
|
|
|
macro3.lean
|
|
|
|
macro_macro.lean
|
|
|
|
macroid.lean
|
|
|
|
macroParams.lean
|
|
|
|
manyAritySyntax.lean
|
|
|
|
mapTR.lean
|
|
|
|
match1.lean
|
chore: fix tests
|
2022-11-30 17:52:37 -08:00 |
|
match_expr.lean
|
feat: expand let_expr macros
|
2024-03-02 08:16:18 -08:00 |
|
match_expr_expected_type_issue.lean
|
fix: propagate expected type at do-match_expr
|
2024-03-02 10:07:15 -08:00 |
|
match_expr_meta_modifier.lean
|
fix: missing atomic at match_expr parser (#3572)
|
2024-03-02 21:55:07 +00:00 |
|
match_expr_perf.lean
|
perf: match_expr join points (#3580)
|
2024-03-03 18:15:49 +00:00 |
|
match_int_lit_issue.lean
|
fix: issue when matching Int literals (#3504)
|
2024-02-26 13:09:07 +00:00 |
|
match_lit_fin_cover.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
match_lit_issues.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
match_lit_regression.lean
|
fix: regression on match expressions with builtin literals (#3521)
|
2024-02-27 18:49:44 +00:00 |
|
match_unit.lean
|
|
|
|
matchArrayLit.lean
|
|
|
|
matchDiscrType.lean
|
|
|
|
matchEqnsHEqIssue.lean
|
|
|
|
matchEqs.lean
|
|
|
|
matchEqsBug.lean
|
|
|
|
matcherElimUniv.lean
|
|
|
|
matchGenBug.lean
|
|
|
|
matchGenIssue.lean
|
|
|
|
matchNoPostponing.lean
|
|
|
|
matchRw.lean
|
|
|
|
matchtac.lean
|
|
|
|
matchUnifyBug.lean
|
|
|
|
matchVarIssue.lean
|
|
|
|
matchWithSearch.lean
|
|
|
|
mathlibetaissue.lean
|
chore: upstream norm_cast tactic (#3322)
|
2024-02-19 17:49:17 -08:00 |
|
mathport18.lean
|
|
|
|
mathport_issue16.lean
|
|
|
|
matrix.lean
|
|
|
|
maze.lean
|
fix: fold raw Nat literals at dsimp (#3624)
|
2024-03-06 18:29:20 +00:00 |
|
mergeSortCPDT.lean
|
chore: upstream omega (#3367)
|
2024-02-19 00:19:55 +00:00 |
|
meta.lean
|
chore: fix more typos in comments
|
2023-10-08 14:37:34 -07:00 |
|
meta1.lean
|
chore: split up & simplify importModules
|
2023-08-31 15:37:33 -04:00 |
|
meta2.lean
|
fix: fold raw Nat literals at dsimp (#3624)
|
2024-03-06 18:29:20 +00:00 |
|
meta3.lean
|
feat: assume function application arguments occurring in local simp theorems have been annotated with no_index (#3406)
|
2024-02-19 12:43:34 -08:00 |
|
meta4.lean
|
|
|
|
meta5.lean
|
|
|
|
meta6.lean
|
|
|
|
meta7.lean
|
chore: fix tests
|
2024-02-18 14:14:55 -08:00 |
|
methodsRetInhabited.lean
|
|
|
|
Miller1.lean
|
|
|
|
missingDeclName.lean
|
|
|
|
missingSizeOfArrayGetThm.lean
|
|
|
|
mixedMacroRules.lean
|
|
|
|
mixfix.lean
|
|
|
|
mjissue.lean
|
|
|
|
modAsClasses.lean
|
|
|
|
monadCache.lean
|
|
|
|
monadControl.lean
|
|
|
|
MonadControl_tutorial.lean
|
|
|
|
monotone.lean
|
|
|
|
mulcomm.lean
|
|
|
|
multiTargetCasesInductionIssue.lean
|
|
|
|
mut_ind_wf.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
mutualDefThms.lean
|
chore: upstream Std.Data.List.Init.Lemmas (#3341)
|
2024-02-15 03:19:23 +00:00 |
|
mutualWithCompositeNames.lean
|
|
|
|
mutwf1.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
mutwf2.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
mutwf3.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
mutwf4.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
namePatEqThm.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
namespaceHyg.lean
|
|
|
|
namespaceIssue.lean
|
|
|
|
namespaceResolution.lean
|
|
|
|
nary_nomatch.lean
|
feat: nary nomatch (#3285)
|
2024-02-09 00:28:34 +00:00 |
|
nat_mod_defeq.lean
|
refactor: redefine Nat.mod such that rfl : 0 % n = 0
|
2023-01-11 09:49:58 -08:00 |
|
nativeReflBackdoor.lean
|
|
|
|
natlit.lean
|
|
|
|
nested_match_bug.lean
|
|
|
|
nestedDo.lean
|
|
|
|
nestedInductiveIssue.lean
|
|
|
|
nestedInductiveRecType.lean
|
|
|
|
nestedIssueMatch.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
nestedrec.lean
|
|
|
|
nestedtc.lean
|
fix: erase *dependent* local instances
|
2023-01-03 11:39:46 -08:00 |
|
nestedWF.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
new_compiler.lean
|
|
|
|
new_frontend2.lean
|
|
|
|
new_inductive.lean
|
|
|
|
new_inductive2.lean
|
|
|
|
newfrontend1.lean
|
|
|
|
newfrontend2.lean
|
|
|
|
newfrontend3.lean
|
feat: type of theorems must be propositions
|
2024-03-13 12:37:58 -07:00 |
|
newfrontend5.lean
|
chore: fix more typos in comments
|
2023-10-08 14:37:34 -07:00 |
|
nicerNestedDos.lean
|
|
|
|
no_simproc_usize.lean
|
fix: disable USize simprocs (#3488)
|
2024-02-24 02:37:39 +00:00 |
|
nofun1.lean
|
feat: nofun tactic and term
|
2024-02-09 15:56:57 +11:00 |
|
noindexAnnotation.lean
|
|
|
|
nomatch_regression.lean
|
fix: nomatch regression (#3296)
|
2024-02-10 04:58:48 +00:00 |
|
nomatch_tac.lean
|
chore: add nomatch tactic (#3294)
|
2024-02-10 04:59:06 +00:00 |
|
noncomp.lean
|
|
|
|
noncomputable_bug.lean
|
|
|
|
nonrec.lean
|
|
|
|
norm_cast.lean
|
chore: upstream norm_cast attributes and tests
|
2024-02-20 07:00:47 -08:00 |
|
numChars.lean
|
|
|
|
obtain.lean
|
|
|
|
offsetIssue.lean
|
|
|
|
ofNat_class.lean
|
|
|
|
ofNatNormNum.lean
|
|
|
|
omega.lean
|
feat: omega doesn't check for defeq atoms (#3525)
|
2024-02-28 05:41:29 +00:00 |
|
omega_examples.lean
|
chore: upstream orphaned tests from Std (#3539)
|
2024-02-29 04:12:52 +00:00 |
|
omegaCanon.lean
|
fix: add Canonicalizer.lean and use it to canonicalize terms in omega (#3639)
|
2024-03-12 23:18:56 +00:00 |
|
openInScopeBug.lean
|
feat: enable failIfUnchanged by default in simp
|
2023-08-16 10:14:23 -07:00 |
|
openTermTactic.lean
|
|
|
|
optParam.lean
|
|
|
|
Ord.lean
|
|
|
|
overAndPartialAppsAtWF.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
overloaded.lean
|
|
|
|
overloadsAndDelayedCoercions.lean
|
|
|
|
panicAtCheckAssignment.lean
|
|
|
|
parray1.lean
|
|
|
|
parsePrelude.lean
|
|
|
|
parserAliasShadow.lean
|
|
|
|
parserQuot.lean
|
|
|
|
partial1.lean
|
|
|
|
partialApp.lean
|
|
|
|
patbug.lean
|
|
|
|
pendingInstBug.lean
|
|
|
|
pendingMVarIssue.lean
|
|
|
|
postponeBinRelIssue.lean
|
|
|
|
posView.lean
|
|
|
|
PPTopDownAnalyze.lean
|
chore: pp.proofs.withType is now false by default (#3379)
|
2024-02-17 15:09:24 +00:00 |
|
precDSL.lean
|
|
|
|
primProjEtaIssue.lean
|
|
|
|
print_cmd.lean
|
|
|
|
printDecls.lean
|
|
|
|
printEqns.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
prioDSL.lean
|
|
|
|
privateCtor.lean
|
|
|
|
processGenDiseqBug.lean
|
|
|
|
projDefEq2.lean
|
|
|
|
proofDataConfusionBug.lean
|
|
|
|
proofIrrelFVar.lean
|
|
|
|
propagateExpectedType.lean
|
|
|
|
prv.lean
|
|
|
|
psumAtWF.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
ptrAddr.lean
|
|
|
|
qualifiedNamesRec.lean
|
|
|
|
quasi_pattern_unification_approx_issue.lean
|
|
|
|
quotInd.lean
|
|
|
|
range.lean
|
|
|
|
rational.lean
|
chore: upstream NatCast and IntCast (#3347)
|
2024-02-16 00:54:22 +00:00 |
|
rawStrings.lean
|
feat: Rust-style raw string literals (#2929)
|
2023-12-20 16:53:08 +00:00 |
|
rc_tests.lean
|
|
|
|
rcases.lean
|
chore: upstream orphaned tests from Std (#3539)
|
2024-02-29 04:12:52 +00:00 |
|
rcases1.lean
|
chore: upstream rcases (#3292)
|
2024-02-10 05:22:02 +00:00 |
|
readerThe.lean
|
|
|
|
recInfo1.lean
|
chore: upstream Std.Logic (#3312)
|
2024-02-14 09:40:55 +00:00 |
|
reduce1.lean
|
|
|
|
reduce2.lean
|
|
|
|
reduce3.lean
|
|
|
|
reductionBug.lean
|
|
|
|
reflectiveIndPred.lean
|
|
|
|
regressions3210.lean
|
fix: Mathlib regressions reported by Scott
|
2024-02-01 16:58:54 +11:00 |
|
Reid1.lean
|
|
|
|
renameI.lean
|
fix: rename_i in macro (#3581)
|
2024-03-03 19:05:37 +00:00 |
|
renaming.lean
|
|
|
|
Reparen.lean
|
fix: parenthesize by optParam values
|
2022-12-20 18:10:39 +01:00 |
|
repeat.lean
|
chore: upstream orphaned tests from Std (#3539)
|
2024-02-29 04:12:52 +00:00 |
|
repeatConv.lean
|
|
|
|
replace.lean
|
|
|
|
replace_tac.lean
|
chore: upstream replace tactic (#3321)
|
2024-02-14 01:53:25 +00:00 |
|
resolveLVal.lean
|
|
|
|
returnOptIssue.lean
|
|
|
|
revert1.lean
|
|
|
|
rewrite.lean
|
chore: basic tests exercising rw
|
2023-08-29 08:07:58 +01:00 |
|
rflProofsCongrCastsIssue.lean
|
|
|
|
robinson.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
root.lean
|
|
|
|
rossel1.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
run_cmd.lean
|
chore: upstream run_cmd and fixes bugs (#3324)
|
2024-02-14 04:15:28 +00:00 |
|
run_meta1.lean
|
fix: run_meta macro (#3334)
|
2024-02-15 00:12:45 +00:00 |
|
rw_inst_implicit_args.lean
|
fix: rewrite tactic should not try to synthesize instances that have been inferred by unification (#3509)
|
2024-02-26 20:18:07 +00:00 |
|
rw_inst_mvars.lean
|
chore: rwa tactic macro (#3299)
|
2024-02-10 04:59:24 +00:00 |
|
rwRegression.lean
|
fix: get_elem_tactic_trivial regression (#3531)
|
2024-02-28 23:14:15 +00:00 |
|
sarray.lean
|
|
|
|
scc.lean
|
|
|
|
scopedCommandAfterOpen.lean
|
|
|
|
scopedHindingIssue.lean
|
|
|
|
scopedParsers.lean
|
|
|
|
scopedParsers2.lean
|
|
|
|
secVarBug.lean
|
|
|
|
set.lean
|
chore: change simp default to decide := false (#2722)
|
2023-11-02 10:06:38 +11:00 |
|
set_lit_unexpand.lean
|
feat: set literal unexpander (#3513)
|
2024-02-27 03:02:41 +00:00 |
|
setOptionTermTactic.lean
|
chore: fix tests
|
2023-11-09 04:06:30 -08:00 |
|
setStructInstNotation.lean
|
chore: set literal notation (#3348)
|
2024-02-19 23:22:36 +00:00 |
|
seval1.lean
|
chore: register seval simp set
|
2024-02-01 16:58:54 +11:00 |
|
sharecommon.lean
|
chore: fix tests
|
2024-02-09 18:23:46 +11:00 |
|
show_term.lean
|
chore: upstream show_term
|
2024-02-29 17:34:15 +11:00 |
|
showTests.lean
|
feat: try to unify show type and expected type
|
2023-01-06 08:48:48 -08:00 |
|
shrinkFn.lean
|
|
|
|
sigmaprec.lean
|
|
|
|
sign.lean
|
|
|
|
simp1.lean
|
refactor: add configuration options to control WHNF
|
2023-10-25 03:12:35 -07:00 |
|
simp2.lean
|
|
|
|
simp3.lean
|
chore: add @[simp] to Nat.succ_eq_add_one, and cleanup downstream (#3579)
|
2024-03-13 05:35:52 +00:00 |
|
simp4.lean
|
chore: upstream Std.Logic (#3312)
|
2024-02-14 09:40:55 +00:00 |
|
simp5.lean
|
|
|
|
simp6.lean
|
chore: upstream Std.Logic (#3312)
|
2024-02-14 09:40:55 +00:00 |
|
simp_all.lean
|
chore: change simp default to decide := false (#2722)
|
2023-11-02 10:06:38 +11:00 |
|
simp_all_contextual.lean
|
|
|
|
simp_eqn_bug.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
simp_failIfUnchanged.lean
|
feat: add failIfUnchanged flag to simp
|
2023-08-13 09:49:25 -07:00 |
|
simp_inst_implict_args.lean
|
fix: simp should not try to synthesize instance implicit arguments that have been inferred by unification (#3507)
|
2024-02-26 20:17:55 +00:00 |
|
simpArith1.lean
|
|
|
|
simpArithCacheIssue.lean
|
fix: simp cache issue
|
2024-02-01 16:58:54 +11:00 |
|
simpAtDefIssue.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
simpAutoUnfold.lean
|
|
|
|
simpBool.lean
|
|
|
|
simpBug.lean
|
|
|
|
simpCasesOnCtorBug.lean
|
|
|
|
simpCnstr1.lean
|
|
|
|
simpCondLemma.lean
|
|
|
|
simpDecide.lean
|
chore: change simp default to decide := false (#2722)
|
2023-11-02 10:06:38 +11:00 |
|
simpDefToUnfold.lean
|
|
|
|
simpDischargeLoop.lean
|
feat: enable failIfUnchanged by default in simp
|
2023-08-16 10:14:23 -07:00 |
|
simpExpBlowup.lean
|
|
|
|
simpExtraArgsBug.lean
|
|
|
|
simpGround1.lean
|
feat: new implementation for simp (config := { ground := true }) (#3187)
|
2024-01-18 17:39:06 +00:00 |
|
simpIfPre.lean
|
feat: replace ite and dite shortcircuit theorems with simproc
|
2024-01-09 12:57:15 +01:00 |
|
simpImpLocal.lean
|
|
|
|
simpInv.lean
|
|
|
|
simpIssue.lean
|
|
|
|
simpJpCasesDepBug.lean
|
|
|
|
simpLoopBug.lean
|
|
|
|
simpMatch.lean
|
|
|
|
simpMatchDiscr.lean
|
|
|
|
simpMatchDiscrIssue.lean
|
feat: better support for match-application in the simplifier
|
2024-01-09 12:57:15 +01:00 |
|
simpOnly.lean
|
|
|
|
simpPartialApp.lean
|
|
|
|
simpPreIssue.lean
|
feat: add reduceStep, and try pre simp steps again if term was reduced
|
2024-01-09 12:57:15 +01:00 |
|
simpPreprocess.lean
|
|
|
|
simpPrio.lean
|
|
|
|
simproc1.lean
|
fix: don't drop doc-comments on simprocs (#3259)
|
2024-02-06 20:31:36 +00:00 |
|
simproc2.lean
|
feat: Int.toNat simproc (#3440)
|
2024-02-21 17:12:14 +00:00 |
|
simproc_builtin_erase.lean
|
feat: use attribute command to add and erase simprocs (#3511)
|
2024-02-26 23:41:49 +00:00 |
|
simproc_disable_issue.lean
|
fix: allow users to disable builtin simprocs in simp args (#3441)
|
2024-02-21 20:01:11 +00:00 |
|
simproc_erase.lean
|
feat: use attribute command to add and erase simprocs (#3511)
|
2024-02-26 23:41:49 +00:00 |
|
simproc_panic.lean
|
chore: upstream (most of) Std.Data.Nat.Lemmas (#3391)
|
2024-02-19 03:47:49 +00:00 |
|
simproc_timeout.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
simpRwBug.lean
|
chore: add @[simp] to Nat.succ_eq_add_one, and cleanup downstream (#3579)
|
2024-03-13 05:35:52 +00:00 |
|
simpStar.lean
|
feat: enable failIfUnchanged by default in simp
|
2023-08-16 10:14:23 -07:00 |
|
simpStarHyp.lean
|
|
|
|
simpUnfoldAbbrev.lean
|
|
|
|
sizeof1.lean
|
|
|
|
sizeof2.lean
|
|
|
|
sizeof3.lean
|
|
|
|
sizeof4.lean
|
|
|
|
sizeof5.lean
|
|
|
|
sizeof6.lean
|
|
|
|
skipAssignedInstances.lean
|
feat: add option tactic.skipAssignedInstances := true for backward compatibilty (#3526)
|
2024-02-28 05:52:29 +00:00 |
|
smartUnfoldingBug.lean
|
|
|
|
solve_by_elim.lean
|
chore: upstream orphaned tests from Std (#3539)
|
2024-02-29 04:12:52 +00:00 |
|
som1.lean
|
|
|
|
spec_issue.lean
|
|
|
|
specbug.lean
|
|
|
|
specialize1.lean
|
|
|
|
specialize2.lean
|
|
|
|
specialize3.lean
|
|
|
|
split1.lean
|
|
|
|
split2.lean
|
|
|
|
split3.lean
|
|
|
|
splitAtCode.lean
|
|
|
|
splitIssue.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
splitList.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
starsAndBars.lean
|
|
|
|
state8.lean
|
|
|
|
state12.lean
|
|
|
|
stateRef.lean
|
|
|
|
streamEqIssue.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
strInterpolation.lean
|
|
|
|
strLitProj.lean
|
|
|
|
struct1.lean
|
|
|
|
struct2.lean
|
|
|
|
struct3.lean
|
|
|
|
struct_inst_typed.lean
|
|
|
|
struct_instance_in_eqn.lean
|
|
|
|
structEqns.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
structInst.lean
|
|
|
|
structInst2.lean
|
|
|
|
structInst3.lean
|
|
|
|
structInst4.lean
|
|
|
|
structInstFast.lean
|
feat: use supplied structure fields left to right and eta reduce terms in structure instance elaboration (#2478)
|
2024-02-01 03:42:39 +00:00 |
|
structNoBody.lean
|
|
|
|
structPrivateFieldBug.lean
|
|
|
|
structPrivateFieldBug2.lean
|
|
|
|
structuralEqns.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
structuralEqns2.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
structuralEqns3.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
structuralIssue.lean
|
|
|
|
structuralIssue2.lean
|
chore: upstream Std.Data.List.Init.Lemmas (#3341)
|
2024-02-15 03:19:23 +00:00 |
|
structuralRec1.lean
|
feat: type of theorems must be propositions
|
2024-03-13 12:37:58 -07:00 |
|
structure.lean
|
|
|
|
structWithAlgTCSynth.lean
|
feat: use supplied structure fields left to right and eta reduce terms in structure instance elaboration (#2478)
|
2024-02-01 03:42:39 +00:00 |
|
stuckMVarBug.lean
|
|
|
|
stuckTC.lean
|
|
|
|
stxKindInsideNamespace.lean
|
|
|
|
stxMacro.lean
|
|
|
|
subexpr.lean
|
|
|
|
subset.lean
|
|
|
|
subst.lean
|
|
|
|
subst1.lean
|
|
|
|
substVars.lean
|
|
|
|
substWithoutExpectedType.lean
|
|
|
|
subtype_inj.lean
|
|
|
|
suffices.lean
|
|
|
|
symm.lean
|
chore: upstream orphaned tests from Std (#3539)
|
2024-02-29 04:12:52 +00:00 |
|
syntax1.lean
|
|
|
|
syntaxAbbrevQuot.lean
|
|
|
|
syntaxPrio.lean
|
|
|
|
synth1.lean
|
feat: reorder tc subgoals according to out-params
|
2023-04-10 13:00:04 -07:00 |
|
synthPending1.lean
|
|
|
|
synthPendingBug.lean
|
|
|
|
tactic.lean
|
|
|
|
tactic1.lean
|
feat: type of theorems must be propositions
|
2024-03-13 12:37:58 -07:00 |
|
tacticExtOverlap.lean
|
|
|
|
tacticTests.lean
|
|
|
|
takeSimpEqns.lean
|
|
|
|
task_test.lean
|
|
|
|
task_test2.lean
|
|
|
|
task_test_io.lean
|
|
|
|
tc_eta_struct_issue.lean
|
Revert "fix: reenable structure eta during tc search"
|
2023-02-09 11:37:30 -08:00 |
|
tcUnivIssue.lean
|
|
|
|
termElab.lean
|
|
|
|
termParserAttr.lean
|
|
|
|
TermSeq.lean
|
|
|
|
test_single.sh
|
fix: revert shared library split on non-Windows platforms (#3529)
|
2024-02-29 19:15:01 +00:00 |
|
thmIsProp.lean
|
feat: type of theorems must be propositions
|
2024-03-13 12:37:58 -07:00 |
|
toArrayEq.lean
|
|
|
|
toDeclEtaBug.lean
|
|
|
|
toExpr.lean
|
|
|
|
toFromJson.lean
|
feat: upstreaming the json% term elaborator (#3265)
|
2024-02-08 03:30:41 +00:00 |
|
toLCNFCacheBug.lean
|
|
|
|
trace.lean
|
|
|
|
traceElabIssue.lean
|
|
|
|
trans.lean
|
|
|
|
treeNode.lean
|
|
|
|
tryHeuristicPerfIssue.lean
|
|
|
|
tryHeuristicPerfIssue2.lean
|
|
|
|
tryPostponeIssue.lean
|
|
|
|
type_class_performance1.lean
|
|
|
|
typeAscImp.lean
|
|
|
|
typeclass_append.lean
|
|
|
|
typeclass_coerce.lean
|
feat: reorder tc subgoals according to out-params
|
2023-04-10 13:00:04 -07:00 |
|
typeclass_diamond.lean
|
|
|
|
typeclass_easy.lean
|
|
|
|
typeclass_loop.lean
|
|
|
|
typeclass_metas_internal_goals1.lean
|
feat: reorder tc subgoals according to out-params
|
2023-04-10 13:00:04 -07:00 |
|
typeclass_metas_internal_goals2.lean
|
feat: reorder tc subgoals according to out-params
|
2023-04-10 13:00:04 -07:00 |
|
typeclass_metas_internal_goals3.lean
|
feat: reorder tc subgoals according to out-params
|
2023-04-10 13:00:04 -07:00 |
|
typeclass_metas_internal_goals4.lean
|
feat: reorder tc subgoals according to out-params
|
2023-04-10 13:00:04 -07:00 |
|
typeclass_outparam.lean
|
|
|
|
ubscalar.lean
|
|
|
|
unexpected_result_with_bind.lean
|
|
|
|
unfoldMany.lean
|
|
|
|
unfoldr.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
unif_issue.lean
|
|
|
|
unif_issue2.lean
|
|
|
|
unifhint1.lean
|
|
|
|
unifhint2.lean
|
|
|
|
unifhint3.lean
|
|
|
|
unihint.lean
|
|
|
|
univIssue.lean
|
|
|
|
univPolyEnum.lean
|
|
|
|
unsafeConst.lean
|
|
|
|
unsafeInit.lean
|
|
|
|
unsafeTerm.lean
|
chore: cleanup and move unsafe term elaborator to BuiltinNotation
|
2024-02-09 18:23:46 +11:00 |
|
update.lean
|
|
|
|
utf8英語.lean
|
|
|
|
wfEqns1.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
wfEqns2.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
wfEqns3.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
wfEqns4.lean
|
chore: rename automatically generated equational theorems (#3661)
|
2024-03-13 07:56:27 +00:00 |
|
wfEqnsIssue.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
wfForIn.lean
|
|
|
|
wfLean3Issue.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
wfOmega.lean
|
feat: use omega in default decreasing_trivial (#3503)
|
2024-02-27 18:53:36 +00:00 |
|
wfOverapplicationIssue.lean
|
refactor: drop sizeOf_get_lt, duplicate of sizeOf_get (#3481)
|
2024-02-23 18:43:28 +00:00 |
|
wfrecUnary.lean
|
feat: drop support for termination_by' (#3033)
|
2023-12-11 17:33:17 +00:00 |
|
WFRelSearch.lean
|
|
|
|
wfSum.lean
|
feat: per-function termination hints
|
2024-01-10 17:27:35 +01:00 |
|
where1.lean
|
chore: add @[simp] to Nat.succ_eq_add_one, and cleanup downstream (#3579)
|
2024-03-13 05:35:52 +00:00 |
|
whileRepeat.lean
|
|
|
|
whnfDelayedMVarIssue.lean
|
|
|
|
WindowsNewlines.lean
|
|
|
|
withReducibleAndInstancesCrash.lean
|
|
|
|
zeroExitPoints.lean
|
|
|
|
zetaDelta.lean
|
chore: fix tests
|
2024-02-18 14:14:55 -08:00 |
|
zetaDeltaIssue.lean
|
fix: zetaDelta := false regression (#3459)
|
2024-02-22 19:10:02 +00:00 |
|
zetaDSimpIssue.lean
|
fix: dsimp zeta bug
|
2024-02-18 14:14:55 -08:00 |
